MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexn0 Structured version   Visualization version   GIF version

Theorem rexn0 4517
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.)
Assertion
Ref Expression
rexn0 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0
StepHypRef Expression
1 dfrex2 3071 . . 3 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
2 rzal 4515 . . . 4 (𝐴 = ∅ → ∀𝑥𝐴 ¬ 𝜑)
32con3i 154 . . 3 (¬ ∀𝑥𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
41, 3sylbi 217 . 2 (∃𝑥𝐴 𝜑 → ¬ 𝐴 = ∅)
54neqned 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