Theorem r19.2zb

Description: A response to the notion that the condition A =/= (/) can be removed in r19.2z . Interestingly enough, ph does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009)

	Ref	Expression
Assertion	r19.2zb	|- ( A =/= (/) <-> ( A. x e. A ph -> E. x e. A ph ) )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	|- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph )
2	1	ex	|- ( A =/= (/) -> ( A. x e. A ph -> E. x e. A ph ) )
3		noel	|- -. x e. (/)
4	3	pm2.21i	|- ( x e. (/) -> ph )
5	4	rgen	|- A. x e. (/) ph
6		raleq	|- ( A = (/) -> ( A. x e. A ph <-> A. x e. (/) ph ) )
7	5 6	mpbiri	|- ( A = (/) -> A. x e. A ph )
8	7	necon3bi	|- ( -. A. x e. A ph -> A =/= (/) )
9		exsimpl	|- ( E. x ( x e. A /\ ph ) -> E. x x e. A )
10		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
11		n0	|- ( A =/= (/) <-> E. x x e. A )
12	9 10 11	3imtr4i	|- ( E. x e. A ph -> A =/= (/) )
13	8 12	ja	|- ( ( A. x e. A ph -> E. x e. A ph ) -> A =/= (/) )
14	2 13	impbii	|- ( A =/= (/) <-> ( A. x e. A ph -> E. x e. A ph ) )