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		noel	$$⊢\neg x\in \varnothing$$
4	3	pm2.21i	$$⊢x\in \varnothing \to \phi$$
5	4	rgen	$$⊢\forall x\in \varnothing \phi$$
6		raleq	$$⊢A=\varnothing \to \left(\forall x\in A\phi \leftrightarrow \forall x\in \varnothing \phi \right)$$
7	5 6	mpbiri	$$⊢A=\varnothing \to \forall x\in A\phi$$
8	7	necon3bi	$$⊢\neg \forall x\in A\phi \to A\ne \varnothing$$
9		exsimpl	$$⊢\exists x\left(x\in A\wedge \phi \right)\to \exists xx\in A$$
10		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
11		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
12	9 10 11	3imtr4i	$$⊢\exists x\in A\phi \to A\ne \varnothing$$
13	8 12	ja	$$⊢\left(\forall x\in A\phi \to \exists x\in A\phi \right)\to A\ne \varnothing$$
14	2 13	impbii	$$⊢A\ne \varnothing \leftrightarrow \left(\forall x\in A\phi \to \exists x\in A\phi \right)$$