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

Theorem rexn0 3878
Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
Assertion
Ref Expression
rexn0  |-  ( E. x  e.  A  ph  ->  A  =/=  (/) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rexn0
StepHypRef Expression
1 ne0i 3746 . . 3  |-  ( x  e.  A  ->  A  =/=  (/) )
21a1d 26 . 2  |-  ( x  e.  A  ->  ( ph  ->  A  =/=  (/) ) )
32rexlimiv 2892 1  |-  ( E. x  e.  A  ph  ->  A  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1844    =/= wne 2600   E.wrex 2757   (/)c0 3740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-v 3063  df-dif 3419  df-nul 3741
This theorem is referenced by:  reusv2lem3  4599  eusvobj2  6273  isdrs2  15894  ismnd  16249  ismndOLD  16252  slwn0  16961  lbsexg  18132  iuncon  20223  grpon0  25631  filbcmb  31526  isbnd2  31574  rencldnfi  35129  iunconlem2  36779  stoweidlem14  37177  2reu4  37576
  Copyright terms: Public domain W3C validator