Theorem rabn0 4317

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

Syntax hints:  ¬ wn 3   ↔ wb 207   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  {crab 3391  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-dif 3886  df-nul 4262

This theorem is referenced by:  class2set  5283  reusv2  5332  exss  5402  frminex  5597  weniso  7298  onminesb  7736  onminsb  7737  onminex  7745  oeeulem  8527  supval2  9358  ordtypelem3  9425  card2on  9459  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  20585  lspf  20964  ordtrest2lem  23186  ordthauslem  23366  1stcfb  23428  2ndcdisj  23439  ptclsg  23598  txconn  23672  txflf  23989  tsmsfbas  24111  iscmet3  25278  minveclem3b  25413  iundisj  25533  dyadmax  25583  dyadmbllem  25584  elqaalem1  26303  elqaalem3  26305  sgmnncl  27128  musum  27172  conway  27789  incistruhgr  29166  uvtx01vtx  29484  spancl  31425  shsval2i  31476  ococin  31497  iundisjf  32678  iundisjfi  32888  ordtrest2NEWlem  34106  esumrnmpt2  34252  esumpinfval  34257  dmsigagen  34328  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemiex  34686  ballotlemsup  34689  bnj110  35040  bnj1204  35194  bnj1253  35199  connpconn  35463  iscvm  35487  wsuclem  36051  weiunlem  36691  poimirlem28  38015  sstotbnd2  38141  igenval  38428  igenidl  38430  pmap0  40257  aks4d1p4  42564  aks4d1p5  42565  aks4d1p7  42568  aks4d1p8  42572  grpods  42679  unitscyglem3  42682  unitscyglem4  42683  fsuppind  43040  pellfundre  43326  pellfundge  43327  pellfundglb  43330  dgraalem  43590  uzwo4  45501  ioodvbdlimc1lem1  46374  fourierdlem31  46581  fourierdlem64  46613  etransclem48  46725  subsaliuncl  46801  smflimlem6  47219  smfpimcc  47251  prmdvdsfmtnof1lem1  48062  prmdvdsfmtnof  48064