Theorem sbceq1a

Description: Equality theorem for class substitution. Class version of sbequ12 . (Contributed by NM, 26-Sep-2003)

	Ref	Expression
Assertion	sbceq1a	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbid	⊢ ( [ 𝑥 / 𝑥 ] 𝜑 ↔ 𝜑 )
2		dfsbcq2	⊢ ( 𝑥 = 𝐴 → ( [ 𝑥 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3	1 2	bitr3id	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )