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

Theorem rabn0 3949
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 3948 . . 3 ({𝑥𝐴𝜑} = ∅ ↔ ∀𝑥𝐴 ¬ 𝜑)
21necon3abii 2837 . 2 ({𝑥𝐴𝜑} ≠ ∅ ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
3 dfrex2 2993 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
42, 3bitr4i 267 1 ({𝑥𝐴𝜑} ≠ ∅ ↔ ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wne 2791  wral 2909  wrex 2910  {crab 2913  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-nul 3908
This theorem is referenced by:  class2set  4823  reusv2  4865  exss  4922  frminex  5084  weniso  6589  onminesb  6983  onminsb  6984  onminex  6992  oeeulem  7666  supval2  8346  ordtypelem3  8410  card2on  8444  tz9.12lem3  8637  rankf  8642  scott0  8734  karden  8743  cardf2  8754  cardval3  8763  cardmin2  8809  acni3  8855  kmlem3  8959  cofsmo  9076  coftr  9080  fin23lem7  9123  enfin2i  9128  axcc4  9246  axdc3lem4  9260  ac6num  9286  pwfseqlem3  9467  wuncval  9549  wunccl  9551  tskmcl  9648  infm3  10967  nnwos  11740  zsupss  11762  zmin  11769  rpnnen1lem2  11799  rpnnen1lem1  11800  rpnnen1lem3  11801  rpnnen1lem5  11803  rpnnen1lem1OLD  11806  rpnnen1lem3OLD  11807  rpnnen1lem5OLD  11809  ioo0  12185  ico0  12206  ioc0  12207  icc0  12208  bitsfzolem  15137  lcmcllem  15290  fissn0dvdsn0  15314  odzcllem  15478  vdwnn  15683  ram0  15707  ramsey  15715  sylow2blem3  18018  iscyg2  18265  pgpfac1lem5  18459  ablfaclem2  18466  ablfaclem3  18467  ablfac  18468  lspf  18955  ordtrest2lem  20988  ordthauslem  21168  1stcfb  21229  2ndcdisj  21240  ptclsg  21399  txconn  21473  txflf  21791  tsmsfbas  21912  iscmet3  23072  minveclem3b  23180  iundisj  23297  dyadmax  23347  dyadmbllem  23348  elqaalem1  24055  elqaalem3  24057  sgmnncl  24854  musum  24898  incistruhgr  25955  uvtxa01vtx0  26278  spancl  28165  shsval2i  28216  ococin  28237  iundisjf  29374  iundisjfi  29529  ordtrest2NEWlem  29942  esumrnmpt2  30104  esumpinfval  30109  dmsigagen  30181  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemiex  30537  ballotlemsup  30540  bnj110  30902  bnj1204  31054  bnj1253  31059  connpconn  31191  iscvm  31215  wsuclem  31747  wsuclemOLD  31748  conway  31884  poimirlem28  33408  sstotbnd2  33544  igenval  33831  igenidl  33833  pmap0  34870  pellfundre  37264  pellfundge  37265  pellfundglb  37268  dgraalem  37534  rgspncl  37558  uzwo4  39041  ioodvbdlimc1lem1  39909  fourierdlem31  40118  fourierdlem64  40150  etransclem48  40262  subsaliuncl  40339  smflimlem6  40747  smfpimcc  40777  prmdvdsfmtnof1lem1  41261  prmdvdsfmtnof  41263
  Copyright terms: Public domain W3C validator