| 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 2815, ax-8 2121. (Revised by GG, 2-Sep-2024.) |
| Ref | Expression |
|---|---|
| rexn0 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfrex2 3067 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 2 | rzal 4429 | . . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 3 | 2 | con3i 154 | . . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅) |
| 4 | 1, 3 | sylbi 218 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅) |
| 5 | 4 | neqned 2942 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1547 ≠ wne 2935 ∀wral 3054 ∃wrex 3064 ∅c0 4268 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-9 2129 ax-ext 2712 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2719 df-cleq 2732 df-ne 2936 df-ral 3055 df-rex 3065 df-dif 3893 df-nul 4269 |
| This theorem is referenced by: r19.2zb 4435 2reu4 4459 reusv2lem3 5336 eusvobj2 7355 isdrs2 18270 ismnd 18703 slwn0 19588 lbsexg 21164 iunconn 23418 ltsn0 27923 grpon0 30598 filbcmb 38114 isbnd2 38157 rencldnfi 43273 iunconnlem2 45385 stoweidlem14 46464 hoidmvval0 47037 thinciso 49967 |
| Copyright terms: Public domain | W3C validator |