Theorem rabn0 4385

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3431  ∅c0 4322

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-dif 3951  df-nul 4323

This theorem is referenced by:  class2set  5353  reusv2  5401  exss  5463  frminex  5656  weniso  7354  onminesb  7785  onminsb  7786  onminex  7794  oeeulem  8605  supval2  9454  ordtypelem3  9519  card2on  9553  tz9.12lem3  9788  rankf  9793  scott0  9885  karden  9894  cardf2  9942  cardval3  9951  cardmin2  9998  acni3  10046  kmlem3  10151  cofsmo  10268  coftr  10272  fin23lem7  10315  enfin2i  10320  axcc4  10438  axdc3lem4  10452  ac6num  10478  pwfseqlem3  10659  wuncval  10741  wunccl  10743  tskmcl  10840  infm3  12178  nnwos  12904  zsupss  12926  zmin  12933  rpnnen1lem2  12966  rpnnen1lem1  12967  rpnnen1lem3  12968  rpnnen1lem5  12970  ioo0  13354  ico0  13375  ioc0  13376  icc0  13377  bitsfzolem  16380  lcmcllem  16538  fissn0dvdsn0  16562  odzcllem  16730  vdwnn  16936  ram0  16960  ramsey  16968  sylow2blem3  19532  iscyg2  19792  pgpfac1lem5  19991  ablfaclem2  19998  ablfaclem3  19999  ablfac  20000  lspf  20730  ordtrest2lem  22928  ordthauslem  23108  1stcfb  23170  2ndcdisj  23181  ptclsg  23340  txconn  23414  txflf  23731  tsmsfbas  23853  iscmet3  25042  minveclem3b  25177  iundisj  25298  dyadmax  25348  dyadmbllem  25349  elqaalem1  26069  elqaalem3  26071  sgmnncl  26888  musum  26932  conway  27538  incistruhgr  28607  uvtx01vtx  28922  spancl  30857  shsval2i  30908  ococin  30929  iundisjf  32088  iundisjfi  32275  ordtrest2NEWlem  33201  esumrnmpt2  33365  esumpinfval  33370  dmsigagen  33441  ballotlemfc0  33790  ballotlemfcc  33791  ballotlemiex  33799  ballotlemsup  33802  bnj110  34168  bnj1204  34322  bnj1253  34327  connpconn  34525  iscvm  34549  wsuclem  35102  poimirlem28  36820  sstotbnd2  36946  igenval  37233  igenidl  37235  pmap0  38940  aks4d1p4  41251  aks4d1p5  41252  aks4d1p7  41255  aks4d1p8  41259  fsuppind  41465  pellfundre  41922  pellfundge  41923  pellfundglb  41926  dgraalem  42190  rgspncl  42214  uzwo4  44042  ioodvbdlimc1lem1  44946  fourierdlem31  45153  fourierdlem64  45185  etransclem48  45297  subsaliuncl  45373  smflimlem6  45791  smfpimcc  45823  prmdvdsfmtnof1lem1  46551  prmdvdsfmtnof  46553