Theorem rabn0 3912

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

Syntax hints:  ¬ wn 3   ↔ wb 195   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  class2set  4758  reusv2  4800  exss  4858  frminex  5018  weniso  6504  onminesb  6890  onminsb  6891  onminex  6899  oeeulem  7568  supval2  8244  ordtypelem3  8308  card2on  8342  tz9.12lem3  8535  rankf  8540  scott0  8632  karden  8641  cardf2  8652  cardval3  8661  cardmin2  8707  acni3  8753  kmlem3  8857  cofsmo  8974  coftr  8978  fin23lem7  9021  enfin2i  9026  axcc4  9144  axdc3lem4  9158  ac6num  9184  pwfseqlem3  9361  wuncval  9443  wunccl  9445  tskmcl  9542  infm3  10861  nnwos  11631  zsupss  11653  zmin  11660  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  bitsfzolem  14994  lcmcllem  15147  fissn0dvdsn0  15171  odzcllem  15335  vdwnn  15540  ram0  15564  ramsey  15572  sylow2blem3  17860  iscyg2  18107  pgpfac1lem5  18301  ablfaclem2  18308  ablfaclem3  18309  ablfac  18310  lspf  18795  ordtrest2lem  20817  ordthauslem  20997  1stcfb  21058  2ndcdisj  21069  ptclsg  21228  txcon  21302  txflf  21620  tsmsfbas  21741  iscmet3  22899  minveclem3b  23007  iundisj  23123  dyadmax  23172  dyadmbllem  23173  elqaalem1  23878  elqaalem3  23880  sgmnncl  24673  musum  24717  incistruhgr  25746  uvtx01vtx  26020  spancl  27579  shsval2i  27630  ococin  27651  iundisjf  28784  iundisjfi  28942  ordtrest2NEWlem  29296  esumrnmpt2  29457  esumpinfval  29462  dmsigagen  29534  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemiex  29890  ballotlemsup  29893  bnj110  30182  bnj1204  30334  bnj1253  30339  conpcon  30471  iscvm  30495  wsuclem  31017  wsuclemOLD  31018  nodenselem4  31083  poimirlem28  32607  sstotbnd2  32743  igenval  33030  igenidl  33032  pmap0  34069  pellfundre  36463  pellfundge  36464  pellfundglb  36467  dgraalem  36734  rgspncl  36758  uzwo4  38246  ioodvbdlimc1lem1  38821  fourierdlem31  39031  fourierdlem64  39063  etransclem48  39175  subsaliuncl  39252  smflimlem6  39662  prmdvdsfmtnof1lem1  40034  prmdvdsfmtnof  40036  uvtxa01vtx0  40623