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

Theorem rabn0 4350
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 4349 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 2991 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 3077 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 278 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wne 2944  wral 3065  wrex 3074  {crab 3410  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-dif 3918  df-nul 4288
This theorem is referenced by:  class2set  5315  reusv2  5363  exss  5425  frminex  5618  weniso  7304  onminesb  7733  onminsb  7734  onminex  7742  oeeulem  8553  supval2  9398  ordtypelem3  9463  card2on  9497  tz9.12lem3  9732  rankf  9737  scott0  9829  karden  9838  cardf2  9886  cardval3  9895  cardmin2  9942  acni3  9990  kmlem3  10095  cofsmo  10212  coftr  10216  fin23lem7  10259  enfin2i  10264  axcc4  10382  axdc3lem4  10396  ac6num  10422  pwfseqlem3  10603  wuncval  10685  wunccl  10687  tskmcl  10784  infm3  12121  nnwos  12847  zsupss  12869  zmin  12876  rpnnen1lem2  12909  rpnnen1lem1  12910  rpnnen1lem3  12911  rpnnen1lem5  12913  ioo0  13296  ico0  13317  ioc0  13318  icc0  13319  bitsfzolem  16321  lcmcllem  16479  fissn0dvdsn0  16503  odzcllem  16671  vdwnn  16877  ram0  16901  ramsey  16909  sylow2blem3  19411  iscyg2  19666  pgpfac1lem5  19865  ablfaclem2  19872  ablfaclem3  19873  ablfac  19874  lspf  20451  ordtrest2lem  22570  ordthauslem  22750  1stcfb  22812  2ndcdisj  22823  ptclsg  22982  txconn  23056  txflf  23373  tsmsfbas  23495  iscmet3  24673  minveclem3b  24808  iundisj  24928  dyadmax  24978  dyadmbllem  24979  elqaalem1  25695  elqaalem3  25697  sgmnncl  26512  musum  26556  conway  27160  incistruhgr  28072  uvtx01vtx  28387  spancl  30320  shsval2i  30371  ococin  30392  iundisjf  31549  iundisjfi  31741  ordtrest2NEWlem  32543  esumrnmpt2  32707  esumpinfval  32712  dmsigagen  32783  ballotlemfc0  33132  ballotlemfcc  33133  ballotlemiex  33141  ballotlemsup  33144  bnj110  33510  bnj1204  33664  bnj1253  33669  connpconn  33869  iscvm  33893  wsuclem  34439  poimirlem28  36135  sstotbnd2  36262  igenval  36549  igenidl  36551  pmap0  38257  aks4d1p4  40565  aks4d1p5  40566  aks4d1p7  40569  aks4d1p8  40573  fsuppind  40794  pellfundre  41233  pellfundge  41234  pellfundglb  41237  dgraalem  41501  rgspncl  41525  uzwo4  43335  ioodvbdlimc1lem1  44246  fourierdlem31  44453  fourierdlem64  44485  etransclem48  44597  subsaliuncl  44673  smflimlem6  45091  smfpimcc  45123  prmdvdsfmtnof1lem1  45850  prmdvdsfmtnof  45852
  Copyright terms: Public domain W3C validator