Metamath Proof Explorer

Theorem pm14.122c

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

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

Step	Hyp	Ref	Expression
1		pm14.122a	\|- ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) ) )
2		pm14.122b	\|- ( A e. V -> ( ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )
3	1 2	bitrd	\|- ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )

Step

Hyp

Ref

Expression

 |-  ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) ) )

 |-  ( A e. V -> ( ( A. x ( ph -> x = A ) /\ [. A / x ]. ph ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )

1 2

 |-  ( A e. V -> ( A. x ( ph <-> x = A ) <-> ( A. x ( ph -> x = A ) /\ E. x ph ) ) )