Theorem pm11.58

Description: Theorem *11.58 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm11.58	|- ( E. x ph <-> E. x E. y ( ph /\ [ y / x ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( ph -> E. x ph )
2		nfv	|- F/ y ph
3	2	sb8e	|- ( E. x ph <-> E. y [ y / x ] ph )
4	1 3	sylib	|- ( ph -> E. y [ y / x ] ph )
5	4	pm4.71i	|- ( ph <-> ( ph /\ E. y [ y / x ] ph ) )
6		19.42v	|- ( E. y ( ph /\ [ y / x ] ph ) <-> ( ph /\ E. y [ y / x ] ph ) )
7	5 6	bitr4i	|- ( ph <-> E. y ( ph /\ [ y / x ] ph ) )
8	7	exbii	|- ( E. x ph <-> E. x E. y ( ph /\ [ y / x ] ph ) )