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

Theorem rexn0 4457
 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 4304 . . 3 (𝑥𝐴𝐴 ≠ ∅)
21a1d 25 . 2 (𝑥𝐴 → (𝜑𝐴 ≠ ∅))
32rexlimiv 3285 1 (∃𝑥𝐴 𝜑𝐴 ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 3021  ∃wrex 3144  ∅c0 4295 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ne 3022  df-ral 3148  df-rex 3149  df-dif 3943  df-nul 4296 This theorem is referenced by:  2reu4  4469  reusv2lem3  5297  eusvobj2  7141  isdrs2  17539  ismnd  17903  slwn0  18660  lbsexg  19856  iunconn  21955  grpon0  28196  filbcmb  34886  isbnd2  34932  rencldnfi  39286  iunconnlem2  41137  stoweidlem14  42168  hoidmvval0  42738
 Copyright terms: Public domain W3C validator