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

Theorem rabn0 4337
Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
Assertion
Ref Expression
rabn0 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)

Proof of Theorem rabn0
StepHypRef Expression
1 rabeq0 4336 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 3060 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 3237 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 280 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wne 3014  wral 3136  wrex 3137  {crab 3140  c0 4289
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-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-dif 3937  df-nul 4290
This theorem is referenced by:  class2set  5245  reusv2  5294  exss  5346  frminex  5528  weniso  7099  onminesb  7505  onminsb  7506  onminex  7514  oeeulem  8219  supval2  8911  ordtypelem3  8976  card2on  9010  tz9.12lem3  9210  rankf  9215  scott0  9307  karden  9316  cardf2  9364  cardval3  9373  cardmin2  9419  acni3  9465  kmlem3  9570  cofsmo  9683  coftr  9687  fin23lem7  9730  enfin2i  9735  axcc4  9853  axdc3lem4  9867  ac6num  9893  pwfseqlem3  10074  wuncval  10156  wunccl  10158  tskmcl  10255  infm3  11592  nnwos  12307  zsupss  12329  zmin  12336  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  ioo0  12755  ico0  12776  ioc0  12777  icc0  12778  bitsfzolem  15775  lcmcllem  15932  fissn0dvdsn0  15956  odzcllem  16121  vdwnn  16326  ram0  16350  ramsey  16358  sylow2blem3  18739  iscyg2  18993  pgpfac1lem5  19193  ablfaclem2  19200  ablfaclem3  19201  ablfac  19202  lspf  19738  ordtrest2lem  21803  ordthauslem  21983  1stcfb  22045  2ndcdisj  22056  ptclsg  22215  txconn  22289  txflf  22606  tsmsfbas  22728  iscmet3  23888  minveclem3b  24023  iundisj  24141  dyadmax  24191  dyadmbllem  24192  elqaalem1  24900  elqaalem3  24902  sgmnncl  25716  musum  25760  incistruhgr  26856  uvtx01vtx  27171  spancl  29105  shsval2i  29156  ococin  29177  iundisjf  30331  iundisjfi  30511  ordtrest2NEWlem  31153  esumrnmpt2  31315  esumpinfval  31320  dmsigagen  31391  ballotlemfc0  31738  ballotlemfcc  31739  ballotlemiex  31747  ballotlemsup  31750  bnj110  32118  bnj1204  32272  bnj1253  32277  connpconn  32470  iscvm  32494  wsuclem  33100  conway  33252  poimirlem28  34907  sstotbnd2  35039  igenval  35326  igenidl  35328  pmap0  36888  pellfundre  39463  pellfundge  39464  pellfundglb  39467  dgraalem  39730  rgspncl  39754  uzwo4  41300  ioodvbdlimc1lem1  42200  fourierdlem31  42408  fourierdlem64  42440  etransclem48  42552  subsaliuncl  42626  smflimlem6  43037  smfpimcc  43067  prmdvdsfmtnof1lem1  43731  prmdvdsfmtnof  43733
  Copyright terms: Public domain W3C validator