Theorem rabn0 4342

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-dif 4050  df-nul 4282

This theorem is used by:  class2set  5323  reusv2  5372  exss  5438  frminex  5637  weniso  7395  onminesb  7841  onminsb  7842  onminex  7850  oeeulem  8648  supval2  9484  ordtypelem3  9551  card2on  9585  tz9.12lem3  9833  rankf  9839  scott0b  9974  scott0OLD  9975  kardenOLD  9997  cardf2  10061  cardval3  10070  cardmin2  10119  acni3  10165  kmlem3  10270  cofsmo  10386  coftr  10390  fin23lem7  10433  enfin2i  10438  axcc4  10556  axdc3lem4  10570  ac6num  10596  pwfseqlem3  10784  wuncval  10866  wunccl  10868  tskmcl  10965  infm3  12316  nnwos  13082  zsupss  13104  zmin  13111  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  ioo0  13541  ico0  13562  ioc0  13563  icc0  13564  bitsfzolem  16648  lcmcllem  16815  fissn0dvdsn0  16839  odzcllem  17014  vdwnn  17220  ram0  17244  ramsey  17252  sylow2blem3  19887  iscyg2  20147  pgpfac1lem5  20346  ablfaclem2  20353  ablfaclem3  20354  ablfac  20355  rgspncl  20916  lspf  21300  ordtrest2lem  23576  ordthauslem  23756  1stcfb  23818  2ndcdisj  23830  ptclsg  23989  txconn  24063  txflf  24380  tsmsfbas  24502  iscmet3  25669  minveclem3b  25804  iundisj  25924  dyadmax  25974  dyadmbllem  25975  elqaalem1  26699  elqaalem3  26701  sgmnncl  27531  musum  27575  conway  28222  incistruhgr  29714  uvtx01vtx  30035  spancl  31995  shsval2i  32046  ococin  32067  iundisjf  33281  iundisjfi  33484  ordtrest2NEWlem  34665  esumrnmpt2  34811  esumpinfval  34816  dmsigagen  34888  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemiex  35245  ballotlemsup  35248  bnj110  35599  bnj1204  35753  bnj1253  35758  connpconn  36208  iscvm  36232  wsuclem  36802  nmuladdel  37176  weiunlem  37466  poimirlem28  38834  sstotbnd2  38974  igenval  39261  igenidl  39263  pmap0  41088  aks4d1p4  43395  aks4d1p5  43396  aks4d1p7  43399  aks4d1p8  43403  grpods  43510  unitscyglem3  43513  unitscyglem4  43514  fsuppind  43884  pellfundre  44154  pellfundge  44155  pellfundglb  44158  dgraalem  44412  uzwo4  46344  ioodvbdlimc1lem1  47214  fourierdlem31  47421  fourierdlem64  47453  etransclem48  47565  subsaliuncl  47641  smflimlem6  48059  smfpimcc  48091  prmdvdsfmtnof1lem1  48942  prmdvdsfmtnof  48944