Theorem rabn0 4339

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 4338	. . 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 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-dif 3902  df-nul 4280

This theorem is used by:  class2set  5319  reusv2  5368  exss  5438  frminex  5634  weniso  7357  onminesb  7792  onminsb  7793  onminex  7801  oeeulem  8589  supval2  9425  ordtypelem3  9492  card2on  9526  tz9.12lem3  9771  rankf  9776  scott0b  9876  scott0OLD  9877  kardenOLD  9899  cardf2  9948  cardval3  9957  cardmin2  10004  acni3  10050  kmlem3  10155  cofsmo  10271  coftr  10275  fin23lem7  10318  enfin2i  10323  axcc4  10441  axdc3lem4  10455  ac6num  10481  pwfseqlem3  10669  wuncval  10751  wunccl  10753  tskmcl  10850  infm3  12198  nnwos  12964  zsupss  12986  zmin  12993  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  ioo0  13423  ico0  13444  ioc0  13445  icc0  13446  bitsfzolem  16524  lcmcllem  16686  fissn0dvdsn0  16710  odzcllem  16884  vdwnn  17090  ram0  17114  ramsey  17122  sylow2blem3  19749  iscyg2  20009  pgpfac1lem5  20208  ablfaclem2  20215  ablfaclem3  20216  ablfac  20217  rgspncl  20775  lspf  21158  ordtrest2lem  23428  ordthauslem  23608  1stcfb  23670  2ndcdisj  23682  ptclsg  23841  txconn  23915  txflf  24232  tsmsfbas  24354  iscmet3  25521  minveclem3b  25656  iundisj  25776  dyadmax  25826  dyadmbllem  25827  elqaalem1  26551  elqaalem3  26553  sgmnncl  27383  musum  27427  conway  28044  incistruhgr  29536  uvtx01vtx  29857  spancl  31817  shsval2i  31868  ococin  31889  iundisjf  33062  iundisjfi  33267  ordtrest2NEWlem  34432  esumrnmpt2  34578  esumpinfval  34583  dmsigagen  34655  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemiex  35013  ballotlemsup  35016  bnj110  35367  bnj1204  35521  bnj1253  35526  connpconn  35814  iscvm  35838  wsuclem  36402  nmuladdel  36792  weiunlem  37082  poimirlem28  38397  sstotbnd2  38524  igenval  38811  igenidl  38813  pmap0  40638  aks4d1p4  42945  aks4d1p5  42946  aks4d1p7  42949  aks4d1p8  42953  grpods  43060  unitscyglem3  43063  unitscyglem4  43064  fsuppind  43436  pellfundre  43722  pellfundge  43723  pellfundglb  43726  dgraalem  43986  uzwo4  45887  ioodvbdlimc1lem1  46759  fourierdlem31  46966  fourierdlem64  46998  etransclem48  47110  subsaliuncl  47186  smflimlem6  47604  smfpimcc  47636  prmdvdsfmtnof1lem1  48487  prmdvdsfmtnof  48489