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

Theorem rexn0 4407
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2812, ax-8 2116. (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 3153 . . 3 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
2 rzal 4405 . . . 4 (𝐴 = ∅ → ∀𝑥𝐴 ¬ 𝜑)
32con3i 157 . . 3 (¬ ∀𝑥𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
41, 3sylbi 220 . 2 (∃𝑥𝐴 𝜑 → ¬ 𝐴 = ∅)
54neqned 2942 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2935  wral 3054  wrex 3055  c0 4221
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 1975  ax-7 2020  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-ne 2936  df-ral 3059  df-rex 3060  df-dif 3856  df-nul 4222
This theorem is referenced by:  2reu4  4423  reusv2lem3  5277  eusvobj2  7176  isdrs2  17678  ismnd  18043  slwn0  18871  lbsexg  20068  iunconn  22192  grpon0  28450  sltn0  33741  filbcmb  35554  isbnd2  35597  rencldnfi  40256  iunconnlem2  42134  stoweidlem14  43138  hoidmvval0  43708
  Copyright terms: Public domain W3C validator