Theorem sbccsb2

Description: Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbccsb2	|- ( [. A / x ]. ph <-> A e. [_ A / x ]_ { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / x ]. ph -> A e. _V )
2		elex	|- ( A e. [_ A / x ]_ { x | ph } -> A e. _V )
3		abid	|- ( x e. { x | ph } <-> ph )
4	3	sbcbii	|- ( [. A / x ]. x e. { x | ph } <-> [. A / x ]. ph )
5		sbcel12	|- ( [. A / x ]. x e. { x | ph } <-> [_ A / x ]_ x e. [_ A / x ]_ { x | ph } )
6		csbvarg	|- ( A e. _V -> [_ A / x ]_ x = A )
7	6	eleq1d	|- ( A e. _V -> ( [_ A / x ]_ x e. [_ A / x ]_ { x | ph } <-> A e. [_ A / x ]_ { x | ph } ) )
8	5 7	bitrid	|- ( A e. _V -> ( [. A / x ]. x e. { x | ph } <-> A e. [_ A / x ]_ { x | ph } ) )
9	4 8	bitr3id	|- ( A e. _V -> ( [. A / x ]. ph <-> A e. [_ A / x ]_ { x | ph } ) )
10	1 2 9	pm5.21nii	|- ( [. A / x ]. ph <-> A e. [_ A / x ]_ { x | ph } )