| 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 2816, ax-8 2110. (Revised by GG, 2-Sep-2024.) |
| Ref | Expression |
|---|---|
| rexn0 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfrex2 3073 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 2 | rzal 4509 | . . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 3 | 2 | con3i 154 | . . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅) |
| 4 | 1, 3 | sylbi 217 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅) |
| 5 | 4 | neqned 2947 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ne 2941 df-ral 3062 df-rex 3071 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: 2reu4 4523 reusv2lem3 5400 eusvobj2 7423 isdrs2 18352 ismnd 18750 slwn0 19633 lbsexg 21166 iunconn 23436 sltn0 27943 grpon0 30521 filbcmb 37747 isbnd2 37790 rencldnfi 42832 iunconnlem2 44955 stoweidlem14 46029 hoidmvval0 46602 thinciso 49117 |
| Copyright terms: Public domain | W3C validator |