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

Metamath Proof Explorer

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		rzal	\|- ( A = (/) -> A. x e. A ph )
4	3	necon3bi	\|- ( -. A. x e. A ph -> A =/= (/) )
5		rexn0	\|- ( E. x e. A ph -> A =/= (/) )
6	4 5	ja	\|- ( ( A. x e. A ph -> E. x e. A ph ) -> A =/= (/) )
7	2 6	impbii	\|- ( A =/= (/) <-> ( A. x e. A ph -> E. x e. A ph ) )