# 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}\ne \varnothing ↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 r19.2z ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
2 1 ex ${⊢}{A}\ne \varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 noel ${⊢}¬{x}\in \varnothing$
4 3 pm2.21i ${⊢}{x}\in \varnothing \to {\phi }$
5 4 rgen ${⊢}\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\phi }$
6 raleq ${⊢}{A}=\varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in \varnothing \phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 5 6 mpbiri ${⊢}{A}=\varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
8 7 necon3bi ${⊢}¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to {A}\ne \varnothing$
9 exsimpl ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
10 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
11 n0 ${⊢}{A}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
12 9 10 11 3imtr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to {A}\ne \varnothing$
13 8 12 ja ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {A}\ne \varnothing$
14 2 13 impbii ${⊢}{A}\ne \varnothing ↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$