This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Restricted existential quantification implies its restriction is
nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) Avoid
df-clel , ax-8 . (Revised by GG, 2-Sep-2024)
|
|
Ref |
Expression |
|
Assertion |
rexn0 |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dfrex2 |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) |
| 2 |
|
rzal |
⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) |
| 3 |
2
|
con3i |
⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅ ) |
| 4 |
1 3
|
sylbi |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅ ) |
| 5 |
4
|
neqned |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅ ) |