Theorem rabn0 4330

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 4329	. . 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 3390  ∅c0 4274

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 3391  df-dif 3893  df-nul 4275

This theorem is referenced by:  class2set  5292  reusv2  5340  exss  5410  frminex  5603  weniso  7302  onminesb  7740  onminsb  7741  onminex  7749  oeeulem  8530  supval2  9361  ordtypelem3  9428  card2on  9462  tz9.12lem3  9704  rankf  9709  scott0  9801  karden  9810  cardf2  9858  cardval3  9867  cardmin2  9914  acni3  9960  kmlem3  10066  cofsmo  10182  coftr  10186  fin23lem7  10229  enfin2i  10234  axcc4  10352  axdc3lem4  10366  ac6num  10392  pwfseqlem3  10574  wuncval  10656  wunccl  10658  tskmcl  10755  infm3  12106  nnwos  12856  zsupss  12878  zmin  12885  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  bitsfzolem  16394  lcmcllem  16556  fissn0dvdsn0  16580  odzcllem  16754  vdwnn  16960  ram0  16984  ramsey  16992  sylow2blem3  19588  iscyg2  19848  pgpfac1lem5  20047  ablfaclem2  20054  ablfaclem3  20055  ablfac  20056  rgspncl  20581  lspf  20960  ordtrest2lem  23178  ordthauslem  23358  1stcfb  23420  2ndcdisj  23431  ptclsg  23590  txconn  23664  txflf  23981  tsmsfbas  24103  iscmet3  25270  minveclem3b  25405  iundisj  25525  dyadmax  25575  dyadmbllem  25576  elqaalem1  26296  elqaalem3  26298  sgmnncl  27124  musum  27168  conway  27785  incistruhgr  29162  uvtx01vtx  29480  spancl  31422  shsval2i  31473  ococin  31494  iundisjf  32674  iundisjfi  32884  ordtrest2NEWlem  34082  esumrnmpt2  34228  esumpinfval  34233  dmsigagen  34304  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemiex  34662  ballotlemsup  34665  bnj110  35016  bnj1204  35170  bnj1253  35175  connpconn  35433  iscvm  35457  wsuclem  36021  weiunlem  36661  poimirlem28  37983  sstotbnd2  38109  igenval  38396  igenidl  38398  pmap0  40225  aks4d1p4  42532  aks4d1p5  42533  aks4d1p7  42536  aks4d1p8  42540  grpods  42647  unitscyglem3  42650  unitscyglem4  42651  fsuppind  43037  pellfundre  43327  pellfundge  43328  pellfundglb  43331  dgraalem  43591  uzwo4  45502  ioodvbdlimc1lem1  46377  fourierdlem31  46584  fourierdlem64  46616  etransclem48  46728  subsaliuncl  46804  smflimlem6  47222  smfpimcc  47254  prmdvdsfmtnof1lem1  48059  prmdvdsfmtnof  48061