Theorem rabn0 4293

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-dif 3884  df-nul 4244

This theorem is referenced by:  class2set  5219  reusv2  5269  exss  5320  frminex  5499  weniso  7086  onminesb  7493  onminsb  7494  onminex  7502  oeeulem  8210  supval2  8903  ordtypelem3  8968  card2on  9002  tz9.12lem3  9202  rankf  9207  scott0  9299  karden  9308  cardf2  9356  cardval3  9365  cardmin2  9412  acni3  9458  kmlem3  9563  cofsmo  9680  coftr  9684  fin23lem7  9727  enfin2i  9732  axcc4  9850  axdc3lem4  9864  ac6num  9890  pwfseqlem3  10071  wuncval  10153  wunccl  10155  tskmcl  10252  infm3  11587  nnwos  12303  zsupss  12325  zmin  12332  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  ioo0  12751  ico0  12772  ioc0  12773  icc0  12774  bitsfzolem  15773  lcmcllem  15930  fissn0dvdsn0  15954  odzcllem  16119  vdwnn  16324  ram0  16348  ramsey  16356  sylow2blem3  18739  iscyg2  18994  pgpfac1lem5  19194  ablfaclem2  19201  ablfaclem3  19202  ablfac  19203  lspf  19739  ordtrest2lem  21808  ordthauslem  21988  1stcfb  22050  2ndcdisj  22061  ptclsg  22220  txconn  22294  txflf  22611  tsmsfbas  22733  iscmet3  23897  minveclem3b  24032  iundisj  24152  dyadmax  24202  dyadmbllem  24203  elqaalem1  24915  elqaalem3  24917  sgmnncl  25732  musum  25776  incistruhgr  26872  uvtx01vtx  27187  spancl  29119  shsval2i  29170  ococin  29191  iundisjf  30352  iundisjfi  30545  ordtrest2NEWlem  31275  esumrnmpt2  31437  esumpinfval  31442  dmsigagen  31513  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemiex  31869  ballotlemsup  31872  bnj110  32240  bnj1204  32394  bnj1253  32399  connpconn  32595  iscvm  32619  wsuclem  33225  conway  33377  poimirlem28  35085  sstotbnd2  35212  igenval  35499  igenidl  35501  pmap0  37061  fsuppind  39456  pellfundre  39822  pellfundge  39823  pellfundglb  39826  dgraalem  40089  rgspncl  40113  uzwo4  41687  ioodvbdlimc1lem1  42573  fourierdlem31  42780  fourierdlem64  42812  etransclem48  42924  subsaliuncl  42998  smflimlem6  43409  smfpimcc  43439  prmdvdsfmtnof1lem1  44101  prmdvdsfmtnof  44103