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 \neq \emptyset \leftrightarrow (\forall x \in A φ \to \exists x \in A φ)$

Proof

Step	Hyp	Ref	Expression
1		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A φ) \to \exists x \in A φ$
2	1	ex	$⊢ A \neq \emptyset \to (\forall x \in A φ \to \exists x \in A φ)$
3		rzal	$⊢ A = \emptyset \to \forall x \in A φ$
4	3	necon3bi	$⊢ \neg \forall x \in A φ \to A \neq \emptyset$
5		rexn0	$⊢ \exists x \in A φ \to A \neq \emptyset$
6	4 5	ja	$⊢ (\forall x \in A φ \to \exists x \in A φ) \to A \neq \emptyset$
7	2 6	impbii	$⊢ A \neq \emptyset \leftrightarrow (\forall x \in A φ \to \exists x \in A φ)$

Metamath Proof Explorer

Theorem r19.2zb

Proof