I don't understand how to handle substitutions in Metamath. If I use stdpc7 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑)),
how do I then actually change y to x in 𝜑? I don't see any suitable theorems to use. Like for instance: [𝑥 / 𝑦] (𝜑 ↔ 𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ), [𝑥 / 𝑦] (𝜑 ∧ 𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ). -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dd7c2190-1be9-491e-a385-aae95318fdc9%40googlegroups.com.
