Theorem sbceq1a

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

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

Proof

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