Theorem rabn0 4343

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  ∅c0 4287

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-dif 3906  df-nul 4288

This theorem is referenced by:  class2set  5302  reusv2  5350  exss  5418  frminex  5611  weniso  7310  onminesb  7748  onminsb  7749  onminex  7757  oeeulem  8539  supval2  9370  ordtypelem3  9437  card2on  9471  tz9.12lem3  9713  rankf  9718  scott0  9810  karden  9819  cardf2  9867  cardval3  9876  cardmin2  9923  acni3  9969  kmlem3  10075  cofsmo  10191  coftr  10195  fin23lem7  10238  enfin2i  10243  axcc4  10361  axdc3lem4  10375  ac6num  10401  pwfseqlem3  10583  wuncval  10665  wunccl  10667  tskmcl  10764  infm3  12113  nnwos  12840  zsupss  12862  zmin  12869  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  bitsfzolem  16373  lcmcllem  16535  fissn0dvdsn0  16559  odzcllem  16732  vdwnn  16938  ram0  16962  ramsey  16970  sylow2blem3  19563  iscyg2  19823  pgpfac1lem5  20022  ablfaclem2  20029  ablfaclem3  20030  ablfac  20031  rgspncl  20558  lspf  20937  ordtrest2lem  23159  ordthauslem  23339  1stcfb  23401  2ndcdisj  23412  ptclsg  23571  txconn  23645  txflf  23962  tsmsfbas  24084  iscmet3  25261  minveclem3b  25396  iundisj  25517  dyadmax  25567  dyadmbllem  25568  elqaalem1  26295  elqaalem3  26297  sgmnncl  27125  musum  27169  conway  27787  incistruhgr  29164  uvtx01vtx  29482  spancl  31424  shsval2i  31475  ococin  31496  iundisjf  32676  iundisjfi  32887  ordtrest2NEWlem  34100  esumrnmpt2  34246  esumpinfval  34251  dmsigagen  34322  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemiex  34680  ballotlemsup  34683  bnj110  35034  bnj1204  35188  bnj1253  35193  connpconn  35451  iscvm  35475  wsuclem  36039  weiunlem  36679  poimirlem28  37899  sstotbnd2  38025  igenval  38312  igenidl  38314  pmap0  40141  aks4d1p4  42449  aks4d1p5  42450  aks4d1p7  42453  aks4d1p8  42457  grpods  42564  unitscyglem3  42567  unitscyglem4  42568  fsuppind  42948  pellfundre  43238  pellfundge  43239  pellfundglb  43242  dgraalem  43502  uzwo4  45413  ioodvbdlimc1lem1  46289  fourierdlem31  46496  fourierdlem64  46528  etransclem48  46640  subsaliuncl  46716  smflimlem6  47134  smfpimcc  47166  prmdvdsfmtnof1lem1  47944  prmdvdsfmtnof  47946