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

Theorem rexn0 4218
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
Assertion
Ref Expression
rexn0 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0
StepHypRef Expression
1 ne0i 4064 . . 3 (𝑥𝐴𝐴 ≠ ∅)
21a1d 25 . 2 (𝑥𝐴 → (𝜑𝐴 ≠ ∅))
32rexlimiv 3165 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wne 2932  wrex 3051  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-v 3342  df-dif 3718  df-nul 4059
This theorem is referenced by:  reusv2lem3  5020  eusvobj2  6806  isdrs2  17140  ismnd  17498  slwn0  18230  lbsexg  19366  iunconn  21433  grpon0  27665  filbcmb  33848  isbnd2  33895  rencldnfi  37887  iunconnlem2  39670  stoweidlem14  40734  hoidmvval0  41307  2reu4  41696
  Copyright terms: Public domain W3C validator