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	syl5bb	|- ( 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 ) ) )