Metamath Proof Explorer

Theorem sbc5

Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016)

Ref Expression
Assertion sbc5 
|- ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. ph -> A e. _V )
2 exsimpl 
 |-  ( E. x ( x = A /\ ph ) -> E. x x = A )
3 isset 
 |-  ( A e. _V <-> E. x x = A )
4 2 3 sylibr 
 |-  ( E. x ( x = A /\ ph ) -> A e. _V )
5 dfsbcq2 
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
6 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
7 6 anbi1d 
 |-  ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
8 7 exbidv 
 |-  ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
9 sb5 
 |-  ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
10 5 8 9 vtoclbg 
 |-  ( A e. _V -> ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) )
11 1 4 10 pm5.21nii 
 |-  ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) )