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

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

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