Theorem rabn0 4339

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 4338	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	necon3abii 3002	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3		dfrex2 3090	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitr4i 281	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-dif 3902  df-nul 4280

This theorem is used by:  class2set  5316  reusv2  5365  exss  5431  frminex  5630  weniso  7362  onminesb  7805  onminsb  7806  onminex  7814  oeeulem  8603  supval2  9440  ordtypelem3  9507  card2on  9541  tz9.12lem3  9789  rankf  9795  scott0b  9930  scott0OLD  9931  kardenOLD  9953  cardf2  10017  cardval3  10026  cardmin2  10073  acni3  10119  kmlem3  10224  cofsmo  10340  coftr  10344  fin23lem7  10387  enfin2i  10392  axcc4  10510  axdc3lem4  10524  ac6num  10550  pwfseqlem3  10738  wuncval  10820  wunccl  10822  tskmcl  10919  infm3  12269  nnwos  13035  zsupss  13057  zmin  13064  rpnnen1lem2  13098  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  ioo0  13494  ico0  13515  ioc0  13516  icc0  13517  bitsfzolem  16597  lcmcllem  16764  fissn0dvdsn0  16788  odzcllem  16963  vdwnn  17169  ram0  17193  ramsey  17201  sylow2blem3  19829  iscyg2  20089  pgpfac1lem5  20288  ablfaclem2  20295  ablfaclem3  20296  ablfac  20297  rgspncl  20858  lspf  21242  ordtrest2lem  23514  ordthauslem  23694  1stcfb  23756  2ndcdisj  23768  ptclsg  23927  txconn  24001  txflf  24318  tsmsfbas  24440  iscmet3  25607  minveclem3b  25742  iundisj  25862  dyadmax  25912  dyadmbllem  25913  elqaalem1  26635  elqaalem3  26637  sgmnncl  27467  musum  27511  conway  28158  incistruhgr  29650  uvtx01vtx  29971  spancl  31931  shsval2i  31982  ococin  32003  iundisjf  33176  iundisjfi  33381  ordtrest2NEWlem  34547  esumrnmpt2  34693  esumpinfval  34698  dmsigagen  34770  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemiex  35127  ballotlemsup  35130  bnj110  35481  bnj1204  35635  bnj1253  35640  connpconn  35979  iscvm  36003  wsuclem  36567  nmuladdel  36941  weiunlem  37231  poimirlem28  38546  sstotbnd2  38688  igenval  38975  igenidl  38977  pmap0  40802  aks4d1p4  43109  aks4d1p5  43110  aks4d1p7  43113  aks4d1p8  43117  grpods  43224  unitscyglem3  43227  unitscyglem4  43228  fsuppind  43598  pellfundre  43867  pellfundge  43868  pellfundglb  43871  dgraalem  44131  uzwo4  46039  ioodvbdlimc1lem1  46910  fourierdlem31  47117  fourierdlem64  47149  etransclem48  47261  subsaliuncl  47337  smflimlem6  47755  smfpimcc  47787  prmdvdsfmtnof1lem1  48638  prmdvdsfmtnof  48640