This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )