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

Theorem rabn0 3908
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 3907 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 2824 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 2975 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 265 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wne 2776  wral 2892  wrex 2893  {crab 2896  c0 3870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-nul 3871
This theorem is referenced by:  class2set  4750  reusv2  4792  exss  4849  frminex  5005  weniso  6479  onminesb  6864  onminsb  6865  onminex  6873  oeeulem  7542  supval2  8218  ordtypelem3  8282  card2on  8316  tz9.12lem3  8509  rankf  8514  scott0  8606  karden  8615  cardf2  8626  cardval3  8635  cardmin2  8681  acni3  8727  kmlem3  8831  cofsmo  8948  coftr  8952  fin23lem7  8995  enfin2i  9000  axcc4  9118  axdc3lem4  9132  ac6num  9158  pwfseqlem3  9335  wuncval  9417  wunccl  9419  tskmcl  9516  infm3  10828  nnwos  11584  zsupss  11606  zmin  11613  rpnnen1lem2  11643  rpnnen1lem1  11644  rpnnen1lem3  11645  rpnnen1lem5  11647  rpnnen1lem1OLD  11650  rpnnen1lem3OLD  11651  rpnnen1lem5OLD  11653  ioo0  12024  ico0  12045  ioc0  12046  icc0  12047  bitsfzolem  14937  lcmcllem  15090  fissn0dvdsn0  15114  odzcllem  15278  vdwnn  15483  ram0  15507  ramsey  15515  sylow2blem3  17803  iscyg2  18050  pgpfac1lem5  18244  ablfaclem2  18251  ablfaclem3  18252  ablfac  18253  lspf  18738  ordtrest2lem  20756  ordthauslem  20936  1stcfb  20997  2ndcdisj  21008  ptclsg  21167  txcon  21241  txflf  21559  tsmsfbas  21680  iscmet3  22814  minveclem3b  22921  iundisj  23037  dyadmax  23086  dyadmbllem  23087  elqaalem1  23792  elqaalem3  23794  sgmnncl  24587  musum  24631  uvtx01vtx  25783  spancl  27382  shsval2i  27433  ococin  27454  iundisjf  28587  iundisjfi  28745  ordtrest2NEWlem  29099  esumrnmpt2  29260  esumpinfval  29265  dmsigagen  29337  ballotlemfc0  29684  ballotlemfcc  29685  ballotlemiex  29693  ballotlemsup  29696  bnj110  29985  bnj1204  30137  bnj1253  30142  conpcon  30274  iscvm  30298  wsuclem  30820  wsuclemOLD  30821  nodenselem4  30886  poimirlem28  32407  sstotbnd2  32543  igenval  32830  igenidl  32832  pmap0  33869  pellfundre  36263  pellfundge  36264  pellfundglb  36267  dgraalem  36534  rgspncl  36558  uzwo4  38046  ioodvbdlimc1lem1  38622  fourierdlem31  38832  fourierdlem64  38864  etransclem48  38976  subsaliuncl  39053  smflimlem6  39463  prmdvdsfmtnof1lem1  39836  prmdvdsfmtnof  39838  incistruhgr  40304  uvtxa01vtx0  40622
  Copyright terms: Public domain W3C validator