Theorem sbequ12a

Description: An equality theorem for substitution. (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 23-Jun-2019)

	Ref	Expression
Assertion	sbequ12a	⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12r	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
2		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	bitr2d	⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) )