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\ne \varnothing \leftrightarrow \left(\forall x\in A\phi \to \exists x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in A\phi \right)\to \exists x\in A\phi$$
2	1	ex	$$⊢A\ne \varnothing \to \left(\forall x\in A\phi \to \exists x\in A\phi \right)$$
3		rzal	$$⊢A=\varnothing \to \forall x\in A\phi$$
4	3	necon3bi	$$⊢\neg \forall x\in A\phi \to A\ne \varnothing$$
5		rexn0	$$⊢\exists x\in A\phi \to A\ne \varnothing$$
6	4 5	ja	$$⊢\left(\forall x\in A\phi \to \exists x\in A\phi \right)\to A\ne \varnothing$$
7	2 6	impbii	$$⊢A\ne \varnothing \leftrightarrow \left(\forall x\in A\phi \to \exists x\in A\phi \right)$$