Theorem rabn0 4386

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  {crab 3433  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-dif 3952  df-nul 4324

This theorem is referenced by:  class2set  5354  reusv2  5402  exss  5464  frminex  5657  weniso  7351  onminesb  7781  onminsb  7782  onminex  7790  oeeulem  8601  supval2  9450  ordtypelem3  9515  card2on  9549  tz9.12lem3  9784  rankf  9789  scott0  9881  karden  9890  cardf2  9938  cardval3  9947  cardmin2  9994  acni3  10042  kmlem3  10147  cofsmo  10264  coftr  10268  fin23lem7  10311  enfin2i  10316  axcc4  10434  axdc3lem4  10448  ac6num  10474  pwfseqlem3  10655  wuncval  10737  wunccl  10739  tskmcl  10836  infm3  12173  nnwos  12899  zsupss  12921  zmin  12928  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  ioo0  13349  ico0  13370  ioc0  13371  icc0  13372  bitsfzolem  16375  lcmcllem  16533  fissn0dvdsn0  16557  odzcllem  16725  vdwnn  16931  ram0  16955  ramsey  16963  sylow2blem3  19490  iscyg2  19750  pgpfac1lem5  19949  ablfaclem2  19956  ablfaclem3  19957  ablfac  19958  lspf  20585  ordtrest2lem  22707  ordthauslem  22887  1stcfb  22949  2ndcdisj  22960  ptclsg  23119  txconn  23193  txflf  23510  tsmsfbas  23632  iscmet3  24810  minveclem3b  24945  iundisj  25065  dyadmax  25115  dyadmbllem  25116  elqaalem1  25832  elqaalem3  25834  sgmnncl  26651  musum  26695  conway  27301  incistruhgr  28370  uvtx01vtx  28685  spancl  30620  shsval2i  30671  ococin  30692  iundisjf  31851  iundisjfi  32038  ordtrest2NEWlem  32933  esumrnmpt2  33097  esumpinfval  33102  dmsigagen  33173  ballotlemfc0  33522  ballotlemfcc  33523  ballotlemiex  33531  ballotlemsup  33534  bnj110  33900  bnj1204  34054  bnj1253  34059  connpconn  34257  iscvm  34281  wsuclem  34828  poimirlem28  36564  sstotbnd2  36690  igenval  36977  igenidl  36979  pmap0  38684  aks4d1p4  40992  aks4d1p5  40993  aks4d1p7  40996  aks4d1p8  41000  fsuppind  41210  pellfundre  41667  pellfundge  41668  pellfundglb  41671  dgraalem  41935  rgspncl  41959  uzwo4  43788  ioodvbdlimc1lem1  44695  fourierdlem31  44902  fourierdlem64  44934  etransclem48  45046  subsaliuncl  45122  smflimlem6  45540  smfpimcc  45572  prmdvdsfmtnof1lem1  46300  prmdvdsfmtnof  46302