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

Metamath Proof Explorer

Theorem pm14.122b

Description: Theorem *14.122 in WhiteheadRussell p. 185. (Contributed by Andrew Salmon, 9-Jun-2011)

Ref Expression
Assertion pm14.122b 
|- ( A e. V -> ( ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
2 1 imbi2d 
 |-  ( y = A -> ( ( ph -> x = y ) <-> ( ph -> x = A ) ) )
3 2 albidv 
 |-  ( y = A -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = A ) ) )
4 dfsbcq 
 |-  ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
5 4 bibi1d 
 |-  ( y = A -> ( ( [. y / x ]. ph <-> E. x ph ) <-> ( [. A / x ]. ph <-> E. x ph ) ) )
6 3 5 imbi12d 
 |-  ( y = A -> ( ( A. x ( ph -> x = y ) -> ( [. y / x ]. ph <-> E. x ph ) ) <-> ( A. x ( ph -> x = A ) -> ( [. A / x ]. ph <-> E. x ph ) ) ) )
7 sbc5 
 |-  ( [. y / x ]. ph <-> E. x ( x = y /\ ph ) )
8 nfa1 
 |-  F/ x A. x ( ph -> x = y )
9 simpr 
 |-  ( ( x = y /\ ph ) -> ph )
10 ancr 
 |-  ( ( ph -> x = y ) -> ( ph -> ( x = y /\ ph ) ) )
11 10 sps 
 |-  ( A. x ( ph -> x = y ) -> ( ph -> ( x = y /\ ph ) ) )
12 9 11 impbid2 
 |-  ( A. x ( ph -> x = y ) -> ( ( x = y /\ ph ) <-> ph ) )
13 8 12 exbid 
 |-  ( A. x ( ph -> x = y ) -> ( E. x ( x = y /\ ph ) <-> E. x ph ) )
14 7 13 bitrid 
 |-  ( A. x ( ph -> x = y ) -> ( [. y / x ]. ph <-> E. x ph ) )
15 6 14 vtoclg 
 |-  ( A e. V -> ( A. x ( ph -> x = A ) -> ( [. A / x ]. ph <-> E. x ph ) ) )
16 15 pm5.32d 
 |-  ( A e. V -> ( ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )