![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexn0 | Structured version Visualization version GIF version |
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2814, ax-8 2108. (Revised by GG, 2-Sep-2024.) |
Ref | Expression |
---|---|
rexn0 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrex2 3071 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | rzal 4515 | . . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
3 | 2 | con3i 154 | . . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅) |
4 | 1, 3 | sylbi 217 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅) |
5 | 4 | neqned 2945 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1537 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 ∅c0 4339 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-ne 2939 df-ral 3060 df-rex 3069 df-dif 3966 df-nul 4340 |
This theorem is referenced by: 2reu4 4529 reusv2lem3 5406 eusvobj2 7423 isdrs2 18364 ismnd 18763 slwn0 19648 lbsexg 21184 iunconn 23452 sltn0 27958 grpon0 30531 filbcmb 37727 isbnd2 37770 rencldnfi 42809 iunconnlem2 44933 stoweidlem14 45970 hoidmvval0 46543 thinciso 48861 |
Copyright terms: Public domain | W3C validator |