Theorem sbceq2a

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

	Ref	Expression
Assertion	sbceq2a	$$⊢A=x\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbceq1a	$$⊢x=A\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
2	1	eqcoms	$$⊢A=x\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	bicomd	$$⊢A=x\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$