Theorem ne0d 4292

Description: Deduction form of ne0i 4291. 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 4291	. 2 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-dif 3905  df-nul 4284

This theorem is referenced by:  snnzg  4727  prnzg  4731  eqsnd  4782  exss  5403  isofrlem  7274  fvmpocurryd  8201  onnseq  8264  oeoalem  8511  oeoelem  8513  oeeui  8517  nnawordex  8552  omxpenlem  8991  frfi  9169  supgtoreq  9355  infltoreq  9388  cantnfp1lem2  9569  cantnfp1lem3  9570  oemapvali  9574  cantnflem1a  9575  cantnflem1d  9578  cantnflem1  9579  epfrs  9621  dfac9  10028  axdc3lem4  10344  intwun  10626  r1limwun  10627  gruina  10709  grur1a  10710  mulclpi  10784  indpi  10798  supsrlem  11002  axpre-sup  11060  supfirege  12109  uzn0  12749  suprzub  12837  fzn0  13438  flval3  13719  icopnfsup  13769  hashelne0d  14275  dfrtrcl2  14969  01sqrexlem3  15151  isercolllem2  15573  isercolllem3  15574  climsup  15577  mertenslem2  15792  gcdcllem1  16410  pclem  16750  prmreclem1  16828  4sqlem13  16869  vdwmc2  16891  vdwlem6  16898  vdwnnlem3  16909  prmgaplem3  16965  prmgaplem4  16966  mrcflem  17512  mrcval  17516  iscatd2  17587  chnub  18528  mndbn0  18658  grpbn0  18879  issubgrpd2  19055  issubg4  19058  subgint  19063  nmzsubg  19078  cycsubgcl  19119  ghmpreima  19151  gastacl  19222  sylow1lem5  19515  pgpssslw  19527  sylow2alem2  19531  sylow2blem3  19535  fislw  19538  sylow3lem4  19543  torsubg  19767  oddvdssubg  19768  iscygd  19800  iscygodd  19801  dprdsubg  19939  ablfac1eu  19988  simpgnideld  20014  submomnd  20045  01eq0ring  20446  cntzsubrng  20483  cntzsubr  20522  imadrhmcl  20713  primefld  20721  primefld0cl  20722  primefld1cl  20723  abvn0b  20752  suborng  20792  islss4  20896  lss1d  20897  lssintcl  20898  lspsolvlem  21080  lbsextlem1  21096  dflidl2rng  21156  lidlsubg  21161  rhmpreimaidl  21215  zringlpirlem1  21400  ocvlss  21610  lmiclbs  21775  lmisfree  21780  psrbas  21871  mplsubglem  21937  mplind  22006  mhpsubg  22069  mat1ric  22403  dmatsgrp  22415  scmatsgrp  22435  scmatsgrp1  22438  scmatlss  22441  scmatric  22453  cpmatsubgpmat  22636  matcpmric  22675  pmmpric  22739  clscld  22963  2ndcdisj  23372  dfac14lem  23533  opnfbas  23758  isfil2  23772  filn0  23778  filssufilg  23827  rnelfmlem  23868  flimfnfcls  23944  ptcmplem2  23969  clssubg  24025  tgpconncomp  24029  tsmsfbas  24044  ustfilxp  24129  ustne0  24130  xbln0  24330  bln0  24331  metustfbas  24473  metustbl  24482  nrgdomn  24587  icccmplem2  24740  icccmplem3  24741  reconnlem2  24744  phtpcer  24922  reparpht  24926  phtpcco2  24927  pcohtpy  24948  pcorevlem  24954  isclmp  25025  iscmet3lem2  25220  bcthlem4  25255  minveclem3b  25356  ivthlem2  25381  ivthlem3  25382  evthicc  25388  ovollb2  25418  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun2  25435  ioombl1lem4  25490  uniioombllem1  25510  uniioombllem2  25512  uniioombllem6  25517  mbfsup  25593  mbfinf  25594  mbflimsup  25595  itg2monolem1  25679  itg2mono  25682  ulm0  26328  pilem2  26390  pilem3  26391  ftalem3  27013  ftalem4  27014  ftalem5  27015  dchrabs  27199  pntlem3  27548  nocvxminlem  27718  tglnne0  28619  axlowdim1  28938  nvo00  30739  nmorepnf  30746  minvecolem1  30852  wrdpmtrlast  33060  cycpmco2lem5  33097  elrgspnlem1  33207  primefldchr  33265  fldgensdrg  33278  nsgqusf1olem1  33376  intlidl  33383  idlinsubrg  33394  rhmimaidl  33395  ssdifidl  33420  ssdifidlprm  33421  ssmxidl  33437  pidufd  33506  1arithufdlem1  33507  ply1dg1rtn0  33542  ply1degltlss  33555  exsslsb  33607  constrsdrg  33786  ordtconnlem1  33935  rrhre  34032  sigagenval  34151  oddpwdc  34365  bnj1177  35016  bnj1523  35081  rankfilimbi  35110  erdszelem8  35240  txsconnlem  35282  cvxsconn  35285  cvmsss2  35316  cvmliftmolem2  35324  cvmlift2lem12  35356  cvmliftpht  35360  finminlem  36358  onint1  36489  weiunlem2  36503  weiunfr  36507  finxpreclem4  37434  heicant  37701  itg2addnc  37720  ftc1anclem7  37745  ftc1anc  37747  prdsbnd2  37841  lkrlss  39140  pclvalN  39935  dian0  41084  docaclN  41169  dicn0  41237  dihglblem5  41343  dihglb2  41387  doch2val2  41409  dochocss  41411  lclkr  41578  lclkrs  41584  lcfr  41630  aks6d1c6lem3  42211  unitscyglem2  42235  qsalrel  42279  nacsfix  42751  mzpcln0  42767  rencldnfilem  42859  fnwe2lem2  43090  kelac1  43102  harn0  43141  hbtlem2  43163  naddwordnexlem4  43440  omltoe  43446  gneispa  44169  imo72b2lem0  44204  scottrankd  44287  relpfrlem  44992  ubelsupr  45063  suprnmpt  45217  disjinfi  45235  suprubrnmpt2  45295  suprubrnmpt  45296  ssfiunibd  45356  allbutfi  45437  allbutfiinf  45464  uzn0d  45469  uzublem  45474  climinf  45652  limclr  45699  climinf2lem  45750  limsupubuzlem  45756  liminflelimsupuz  45829  cnrefiisplem  45873  ioodvbdlimc1lem1  45975  ioodvbdlimc1  45977  ioodvbdlimc2  45979  stoweidlem36  46080  fourierdlem20  46171  fourierdlem25  46176  fourierdlem31  46182  fourierdlem37  46188  fourierdlem46  46196  fourierdlem52  46202  fourierdlem54  46204  fouriercn  46276  elaa2lem  46277  salgenval  46365  salgenn0  46375  sge0isum  46471  sge0reuzb  46492  ovnlerp  46606  ovnf  46607  hsphoidmvle2  46629  hsphoidmvle  46630  hoiprodp1  46632  hoidmv1lelem1  46635  hoidmv1lelem3  46637  hoidmv1le  46638  hoidifhspdmvle  46664  hspmbllem1  46670  hspmbllem3  46672  ovnovollem2  46701  smflimlem1  46815  smfsuplem1  46855  smfsuplem3  46857  smflimsuplem5  46868  smflimsuplem7  46870  preimafvn0  47417  lincolss  48472  fvconstr2  48901  catprs  49049  discsubc  49102  iinfconstbas  49104  eloppf  49171  eloppf2  49172  oppcup3  49247  oppcthinendcALT  49479  termcterm3  49553  termcciso  49554  idfudiag1bas  49562  idfudiag1  49563