Theorem ne0d 4283

Description: Deduction form of ne0i 4282. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
ne0d.1	⊢ (𝜑 → 𝐵 ∈ 𝐴)

Assertion

Ref	Expression
ne0d	⊢ (𝜑 → 𝐴 ≠ ∅)

Proof of Theorem ne0d

Step	Hyp	Ref	Expression
1		ne0d.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
2		ne0i 4282	. 2 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ∅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-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3893  df-nul 4275

This theorem is referenced by:  snnzg  4719  prnzg  4723  eqsnd  4774  exss  5410  isofrlem  7288  fvmpocurryd  8214  onnseq  8277  oeoalem  8525  oeoelem  8527  oeeui  8531  nnawordex  8566  omxpenlem  9009  frfi  9188  supgtoreq  9377  infltoreq  9410  cantnfp1lem2  9591  cantnfp1lem3  9592  oemapvali  9596  cantnflem1a  9597  cantnflem1d  9600  cantnflem1  9601  epfrs  9643  dfac9  10050  axdc3lem4  10366  intwun  10649  r1limwun  10650  gruina  10732  grur1a  10733  mulclpi  10807  indpi  10821  supsrlem  11025  axpre-sup  11083  supfirege  12134  uzn0  12796  suprzub  12880  fzn0  13483  flval3  13765  icopnfsup  13815  hashelne0d  14321  dfrtrcl2  15015  01sqrexlem3  15197  isercolllem2  15619  isercolllem3  15620  climsup  15623  mertenslem2  15841  gcdcllem1  16459  pclem  16800  prmreclem1  16878  4sqlem13  16919  vdwmc2  16941  vdwlem6  16948  vdwnnlem3  16959  prmgaplem3  17015  prmgaplem4  17016  mrcflem  17563  mrcval  17567  iscatd2  17638  chnub  18579  mndbn0  18709  grpbn0  18933  issubgrpd2  19109  issubg4  19112  subgint  19117  nmzsubg  19131  cycsubgcl  19172  ghmpreima  19204  gastacl  19275  sylow1lem5  19568  pgpssslw  19580  sylow2alem2  19584  sylow2blem3  19588  fislw  19591  sylow3lem4  19596  torsubg  19820  oddvdssubg  19821  iscygd  19853  iscygodd  19854  dprdsubg  19992  ablfac1eu  20041  simpgnideld  20067  submomnd  20098  01eq0ring  20498  cntzsubrng  20535  cntzsubr  20574  imadrhmcl  20765  primefld  20773  primefld0cl  20774  primefld1cl  20775  abvn0b  20804  suborng  20844  islss4  20948  lss1d  20949  lssintcl  20950  lspsolvlem  21132  lbsextlem1  21148  dflidl2rng  21208  lidlsubg  21213  rhmpreimaidl  21267  zringlpirlem1  21452  ocvlss  21662  lmiclbs  21827  lmisfree  21832  psrbas  21923  mplsubglem  21987  mplind  22058  mhpsubg  22129  mat1ric  22462  dmatsgrp  22474  scmatsgrp  22494  scmatsgrp1  22497  scmatlss  22500  scmatric  22512  cpmatsubgpmat  22695  matcpmric  22734  pmmpric  22798  clscld  23022  2ndcdisj  23431  dfac14lem  23592  opnfbas  23817  isfil2  23831  filn0  23837  filssufilg  23886  rnelfmlem  23927  flimfnfcls  24003  ptcmplem2  24028  clssubg  24084  tgpconncomp  24088  tsmsfbas  24103  ustfilxp  24188  ustne0  24189  xbln0  24389  bln0  24390  metustfbas  24532  metustbl  24541  nrgdomn  24646  icccmplem2  24799  icccmplem3  24800  reconnlem2  24803  phtpcer  24972  reparpht  24975  phtpcco2  24976  pcohtpy  24997  pcorevlem  25003  isclmp  25074  iscmet3lem2  25269  bcthlem4  25304  minveclem3b  25405  ivthlem2  25429  ivthlem3  25430  evthicc  25436  ovollb2  25466  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliun2  25483  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem2  25560  uniioombllem6  25565  mbfsup  25641  mbfinf  25642  mbflimsup  25643  itg2monolem1  25727  itg2mono  25730  ulm0  26369  pilem2  26430  pilem3  26431  ftalem3  27052  ftalem4  27053  ftalem5  27054  dchrabs  27237  pntlem3  27586  nocvxminlem  27760  bdayfinbndlem1  28473  tglnne0  28722  axlowdim1  29042  nvo00  30847  nmorepnf  30854  minvecolem1  30960  wrdpmtrlast  33169  cycpmco2lem5  33206  elrgspnlem1  33318  primefldchr  33377  fldgensdrg  33390  nsgqusf1olem1  33488  intlidl  33495  idlinsubrg  33506  rhmimaidl  33507  ssdifidl  33532  ssdifidlprm  33533  ssmxidl  33549  pidufd  33618  1arithufdlem1  33619  ply1dg1rtn0  33656  ply1degltlss  33671  exsslsb  33756  constrsdrg  33935  ordtconnlem1  34084  rrhre  34181  sigagenval  34300  oddpwdc  34514  bnj1177  35164  bnj1523  35229  rankfilimbi  35260  erdszelem8  35396  txsconnlem  35438  cvxsconn  35441  cvmsss2  35472  cvmliftmolem2  35480  cvmlift2lem12  35512  cvmliftpht  35516  finminlem  36516  onint1  36647  weiunlem  36661  weiunfr  36665  finxpreclem4  37724  heicant  37990  itg2addnc  38009  ftc1anclem7  38034  ftc1anc  38036  prdsbnd2  38130  lkrlss  39555  pclvalN  40350  dian0  41499  docaclN  41584  dicn0  41652  dihglblem5  41758  dihglb2  41802  doch2val2  41824  dochocss  41826  lclkr  41993  lclkrs  41999  lcfr  42045  aks6d1c6lem3  42625  unitscyglem2  42649  qsalrel  42694  nacsfix  43158  mzpcln0  43174  rencldnfilem  43266  fnwe2lem2  43497  kelac1  43509  harn0  43548  hbtlem2  43570  naddwordnexlem4  43847  omltoe  43852  gneispa  44575  imo72b2lem0  44610  scottrankd  44693  relpfrlem  45398  ubelsupr  45469  suprnmpt  45622  disjinfi  45640  suprubrnmpt2  45699  suprubrnmpt  45700  ssfiunibd  45760  allbutfi  45840  allbutfiinf  45866  uzn0d  45871  uzublem  45876  climinf  46054  limclr  46101  climinf2lem  46152  limsupubuzlem  46158  liminflelimsupuz  46231  cnrefiisplem  46275  ioodvbdlimc1lem1  46377  ioodvbdlimc1  46379  ioodvbdlimc2  46381  stoweidlem36  46482  fourierdlem20  46573  fourierdlem25  46578  fourierdlem31  46584  fourierdlem37  46590  fourierdlem46  46598  fourierdlem52  46604  fourierdlem54  46606  fouriercn  46678  elaa2lem  46679  salgenval  46767  salgenn0  46777  sge0isum  46873  sge0reuzb  46894  ovnlerp  47008  ovnf  47009  hsphoidmvle2  47031  hsphoidmvle  47032  hoiprodp1  47034  hoidmv1lelem1  47037  hoidmv1lelem3  47039  hoidmv1le  47040  hoidifhspdmvle  47066  hspmbllem1  47072  hspmbllem3  47074  ovnovollem2  47103  smflimlem1  47217  smfsuplem1  47257  smfsuplem3  47259  smflimsuplem5  47270  smflimsuplem7  47272  preimafvn0  47852  lincolss  48922  fvconstr2  49351  catprs  49498  discsubc  49551  iinfconstbas  49553  eloppf  49620  eloppf2  49621  oppcup3  49696  oppcthinendcALT  49928  termcterm3  50002  termcciso  50003  idfudiag1bas  50011  idfudiag1  50012