Theorem rabn0 4395

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3433  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-dif 3966  df-nul 4340

This theorem is referenced by:  class2set  5361  reusv2  5409  exss  5474  frminex  5668  weniso  7374  onminesb  7813  onminsb  7814  onminex  7822  oeeulem  8638  supval2  9493  ordtypelem3  9558  card2on  9592  tz9.12lem3  9827  rankf  9832  scott0  9924  karden  9933  cardf2  9981  cardval3  9990  cardmin2  10037  acni3  10085  kmlem3  10191  cofsmo  10307  coftr  10311  fin23lem7  10354  enfin2i  10359  axcc4  10477  axdc3lem4  10491  ac6num  10517  pwfseqlem3  10698  wuncval  10780  wunccl  10782  tskmcl  10879  infm3  12225  nnwos  12955  zsupss  12977  zmin  12984  rpnnen1lem2  13017  rpnnen1lem1  13018  rpnnen1lem3  13019  rpnnen1lem5  13021  ioo0  13409  ico0  13430  ioc0  13431  icc0  13432  bitsfzolem  16468  lcmcllem  16630  fissn0dvdsn0  16654  odzcllem  16826  vdwnn  17032  ram0  17056  ramsey  17064  sylow2blem3  19655  iscyg2  19915  pgpfac1lem5  20114  ablfaclem2  20121  ablfaclem3  20122  ablfac  20123  rgspncl  20630  lspf  20990  ordtrest2lem  23227  ordthauslem  23407  1stcfb  23469  2ndcdisj  23480  ptclsg  23639  txconn  23713  txflf  24030  tsmsfbas  24152  iscmet3  25341  minveclem3b  25476  iundisj  25597  dyadmax  25647  dyadmbllem  25648  elqaalem1  26376  elqaalem3  26378  sgmnncl  27205  musum  27249  conway  27859  incistruhgr  29111  uvtx01vtx  29429  spancl  31365  shsval2i  31416  ococin  31437  iundisjf  32609  iundisjfi  32804  ordtrest2NEWlem  33883  esumrnmpt2  34049  esumpinfval  34054  dmsigagen  34125  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemiex  34483  ballotlemsup  34486  bnj110  34851  bnj1204  35005  bnj1253  35010  connpconn  35220  iscvm  35244  wsuclem  35807  weiunlem2  36446  poimirlem28  37635  sstotbnd2  37761  igenval  38048  igenidl  38050  pmap0  39748  aks4d1p4  42061  aks4d1p5  42062  aks4d1p7  42065  aks4d1p8  42069  grpods  42176  unitscyglem3  42179  unitscyglem4  42180  fsuppind  42577  pellfundre  42869  pellfundge  42870  pellfundglb  42873  dgraalem  43134  uzwo4  44993  ioodvbdlimc1lem1  45887  fourierdlem31  46094  fourierdlem64  46126  etransclem48  46238  subsaliuncl  46314  smflimlem6  46732  smfpimcc  46764  prmdvdsfmtnof1lem1  47509  prmdvdsfmtnof  47511