Theorem rabn0 4316

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-dif 3886  df-nul 4254

This theorem is referenced by:  class2set  5271  reusv2  5321  exss  5372  frminex  5560  weniso  7205  onminesb  7620  onminsb  7621  onminex  7629  oeeulem  8394  supval2  9144  ordtypelem3  9209  card2on  9243  tz9.12lem3  9478  rankf  9483  scott0  9575  karden  9584  cardf2  9632  cardval3  9641  cardmin2  9688  acni3  9734  kmlem3  9839  cofsmo  9956  coftr  9960  fin23lem7  10003  enfin2i  10008  axcc4  10126  axdc3lem4  10140  ac6num  10166  pwfseqlem3  10347  wuncval  10429  wunccl  10431  tskmcl  10528  infm3  11864  nnwos  12584  zsupss  12606  zmin  12613  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  bitsfzolem  16069  lcmcllem  16229  fissn0dvdsn0  16253  odzcllem  16421  vdwnn  16627  ram0  16651  ramsey  16659  sylow2blem3  19142  iscyg2  19397  pgpfac1lem5  19597  ablfaclem2  19604  ablfaclem3  19605  ablfac  19606  lspf  20151  ordtrest2lem  22262  ordthauslem  22442  1stcfb  22504  2ndcdisj  22515  ptclsg  22674  txconn  22748  txflf  23065  tsmsfbas  23187  iscmet3  24362  minveclem3b  24497  iundisj  24617  dyadmax  24667  dyadmbllem  24668  elqaalem1  25384  elqaalem3  25386  sgmnncl  26201  musum  26245  incistruhgr  27352  uvtx01vtx  27667  spancl  29599  shsval2i  29650  ococin  29671  iundisjf  30829  iundisjfi  31019  ordtrest2NEWlem  31774  esumrnmpt2  31936  esumpinfval  31941  dmsigagen  32012  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemiex  32368  ballotlemsup  32371  bnj110  32738  bnj1204  32892  bnj1253  32897  connpconn  33097  iscvm  33121  wsuclem  33746  conway  33920  poimirlem28  35732  sstotbnd2  35859  igenval  36146  igenidl  36148  pmap0  37706  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8  40023  fsuppind  40202  pellfundre  40619  pellfundge  40620  pellfundglb  40623  dgraalem  40886  rgspncl  40910  uzwo4  42490  ioodvbdlimc1lem1  43362  fourierdlem31  43569  fourierdlem64  43601  etransclem48  43713  subsaliuncl  43787  smflimlem6  44198  smfpimcc  44228  prmdvdsfmtnof1lem1  44924  prmdvdsfmtnof  44926