Theorem rabn0 4338

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-dif 4046  df-nul 4278

This theorem is used by:  class2set  5316  reusv2  5365  exss  5431  frminex  5630  weniso  7368  onminesb  7811  onminsb  7812  onminex  7820  oeeulem  8617  supval2  9454  ordtypelem3  9521  card2on  9555  tz9.12lem3  9803  rankf  9809  scott0b  9944  scott0OLD  9945  kardenOLD  9967  cardf2  10031  cardval3  10040  cardmin2  10087  acni3  10133  kmlem3  10238  cofsmo  10354  coftr  10358  fin23lem7  10401  enfin2i  10406  axcc4  10524  axdc3lem4  10538  ac6num  10564  pwfseqlem3  10752  wuncval  10834  wunccl  10836  tskmcl  10933  infm3  12283  nnwos  13049  zsupss  13071  zmin  13078  rpnnen1lem2  13112  rpnnen1lem1  13113  rpnnen1lem3  13114  rpnnen1lem5  13116  ioo0  13508  ico0  13529  ioc0  13530  icc0  13531  bitsfzolem  16613  lcmcllem  16780  fissn0dvdsn0  16804  odzcllem  16979  vdwnn  17185  ram0  17209  ramsey  17217  sylow2blem3  19845  iscyg2  20105  pgpfac1lem5  20304  ablfaclem2  20311  ablfaclem3  20312  ablfac  20313  rgspncl  20874  lspf  21258  ordtrest2lem  23530  ordthauslem  23710  1stcfb  23772  2ndcdisj  23784  ptclsg  23943  txconn  24017  txflf  24334  tsmsfbas  24456  iscmet3  25623  minveclem3b  25758  iundisj  25878  dyadmax  25928  dyadmbllem  25929  elqaalem1  26651  elqaalem3  26653  sgmnncl  27483  musum  27527  conway  28174  incistruhgr  29666  uvtx01vtx  29987  spancl  31947  shsval2i  31998  ococin  32019  iundisjf  33234  iundisjfi  33438  ordtrest2NEWlem  34604  esumrnmpt2  34750  esumpinfval  34755  dmsigagen  34827  ballotlemfc0  35175  ballotlemfcc  35176  ballotlemiex  35184  ballotlemsup  35187  bnj110  35538  bnj1204  35692  bnj1253  35697  connpconn  36090  iscvm  36114  wsuclem  36683  nmuladdel  37057  weiunlem  37347  poimirlem28  38675  sstotbnd2  38817  igenval  39104  igenidl  39106  pmap0  40931  aks4d1p4  43238  aks4d1p5  43239  aks4d1p7  43242  aks4d1p8  43246  grpods  43353  unitscyglem3  43356  unitscyglem4  43357  fsuppind  43727  pellfundre  43997  pellfundge  43998  pellfundglb  44001  dgraalem  44256  uzwo4  46178  ioodvbdlimc1lem1  47049  fourierdlem31  47256  fourierdlem64  47288  etransclem48  47400  subsaliuncl  47476  smflimlem6  47894  smfpimcc  47926  prmdvdsfmtnof1lem1  48777  prmdvdsfmtnof  48779