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  27300  incistruhgr  28339  uvtx01vtx  28654  spancl  30589  shsval2i  30640  ococin  30661  iundisjf  31820  iundisjfi  32007  ordtrest2NEWlem  32902  esumrnmpt2  33066  esumpinfval  33071  dmsigagen  33142  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  ballotlemsup  33503  bnj110  33869  bnj1204  34023  bnj1253  34028  connpconn  34226  iscvm  34250  wsuclem  34797  poimirlem28  36516  sstotbnd2  36642  igenval  36929  igenidl  36931  pmap0  38636  aks4d1p4  40944  aks4d1p5  40945  aks4d1p7  40948  aks4d1p8  40952  fsuppind  41162  pellfundre  41619  pellfundge  41620  pellfundglb  41623  dgraalem  41887  rgspncl  41911  uzwo4  43740  ioodvbdlimc1lem1  44647  fourierdlem31  44854  fourierdlem64  44886  etransclem48  44998  subsaliuncl  45074  smflimlem6  45492  smfpimcc  45524  prmdvdsfmtnof1lem1  46252  prmdvdsfmtnof  46254