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	⊢ ( 𝐴 ≠ ∅ ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑥 ∈ 𝐴 𝜑 )
2	1	ex	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
3		noel	⊢ ¬ 𝑥 ∈ ∅
4	3	pm2.21i	⊢ ( 𝑥 ∈ ∅ → 𝜑 )
5	4	rgen	⊢ ∀ 𝑥 ∈ ∅ 𝜑
6		raleq	⊢ ( 𝐴 = ∅ → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ ∅ 𝜑 ) )
7	5 6	mpbiri	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 )
8	7	necon3bi	⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ )
9		exsimpl	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∃ 𝑥 𝑥 ∈ 𝐴 )
10		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
11		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
12	9 10 11	3imtr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ )
13	8 12	ja	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) → 𝐴 ≠ ∅ )
14	2 13	impbii	⊢ ( 𝐴 ≠ ∅ ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )