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

Theorem rexn0 4441
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2816, ax-8 2108. (Revised by Gino Giotto, 2-Sep-2024.)
Assertion
Ref Expression
rexn0 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0
StepHypRef Expression
1 dfrex2 3170 . . 3 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
2 rzal 4439 . . . 4 (𝐴 = ∅ → ∀𝑥𝐴 ¬ 𝜑)
32con3i 154 . . 3 (¬ ∀𝑥𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
41, 3sylbi 216 . 2 (∃𝑥𝐴 𝜑 → ¬ 𝐴 = ∅)
54neqned 2950 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2943  wral 3064  wrex 3065  c0 4256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ne 2944  df-ral 3069  df-rex 3070  df-dif 3890  df-nul 4257
This theorem is referenced by:  2reu4  4457  reusv2lem3  5323  eusvobj2  7268  isdrs2  18024  ismnd  18388  slwn0  19220  lbsexg  20426  iunconn  22579  grpon0  28864  sltn0  34085  filbcmb  35898  isbnd2  35941  rencldnfi  40643  iunconnlem2  42555  stoweidlem14  43555  hoidmvval0  44125  thinciso  46341
  Copyright terms: Public domain W3C validator