Metamath Proof Explorer

Theorem sbceq2a

Description: Equality theorem for class substitution. Class version of sbequ12r . (Contributed by NM, 4-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 sbceq1a ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
2 1 eqcoms ⊢ ( 𝐴 = 𝑥 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3 2 bicomd ⊢ ( 𝐴 = 𝑥 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) )