Theorem rabn0 4341

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

Step	Hyp	Ref	Expression
1		rabeq0 4340	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	necon3abii 3064	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3		dfrex2 3241	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitr4i 280	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208   ≠ wne 3018  ∀wral 3140  ∃wrex 3141  {crab 3144  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-dif 3941  df-nul 4294

This theorem is referenced by:  class2set  5256  reusv2  5306  exss  5357  frminex  5537  weniso  7109  onminesb  7515  onminsb  7516  onminex  7524  oeeulem  8229  supval2  8921  ordtypelem3  8986  card2on  9020  tz9.12lem3  9220  rankf  9225  scott0  9317  karden  9326  cardf2  9374  cardval3  9383  cardmin2  9429  acni3  9475  kmlem3  9580  cofsmo  9693  coftr  9697  fin23lem7  9740  enfin2i  9745  axcc4  9863  axdc3lem4  9877  ac6num  9903  pwfseqlem3  10084  wuncval  10166  wunccl  10168  tskmcl  10265  infm3  11602  nnwos  12318  zsupss  12340  zmin  12347  rpnnen1lem2  12379  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  ioo0  12766  ico0  12787  ioc0  12788  icc0  12789  bitsfzolem  15785  lcmcllem  15942  fissn0dvdsn0  15966  odzcllem  16131  vdwnn  16336  ram0  16360  ramsey  16368  sylow2blem3  18749  iscyg2  19003  pgpfac1lem5  19203  ablfaclem2  19210  ablfaclem3  19211  ablfac  19212  lspf  19748  ordtrest2lem  21813  ordthauslem  21993  1stcfb  22055  2ndcdisj  22066  ptclsg  22225  txconn  22299  txflf  22616  tsmsfbas  22738  iscmet3  23898  minveclem3b  24033  iundisj  24151  dyadmax  24201  dyadmbllem  24202  elqaalem1  24910  elqaalem3  24912  sgmnncl  25726  musum  25770  incistruhgr  26866  uvtx01vtx  27181  spancl  29115  shsval2i  29166  ococin  29187  iundisjf  30341  iundisjfi  30521  ordtrest2NEWlem  31167  esumrnmpt2  31329  esumpinfval  31334  dmsigagen  31405  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemiex  31761  ballotlemsup  31764  bnj110  32132  bnj1204  32286  bnj1253  32291  connpconn  32484  iscvm  32508  wsuclem  33114  conway  33266  poimirlem28  34922  sstotbnd2  35054  igenval  35341  igenidl  35343  pmap0  36903  pellfundre  39485  pellfundge  39486  pellfundglb  39489  dgraalem  39752  rgspncl  39776  uzwo4  41322  ioodvbdlimc1lem1  42223  fourierdlem31  42430  fourierdlem64  42462  etransclem48  42574  subsaliuncl  42648  smflimlem6  43059  smfpimcc  43089  prmdvdsfmtnof1lem1  43753  prmdvdsfmtnof  43755