Theorem ne0d 4294

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2932  ∅c0 4285

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3904  df-nul 4286

This theorem is referenced by:  snnzg  4731  prnzg  4735  eqsnd  4786  exss  5411  isofrlem  7286  fvmpocurryd  8213  onnseq  8276  oeoalem  8524  oeoelem  8526  oeeui  8530  nnawordex  8565  omxpenlem  9006  frfi  9185  supgtoreq  9374  infltoreq  9407  cantnfp1lem2  9588  cantnfp1lem3  9589  oemapvali  9593  cantnflem1a  9594  cantnflem1d  9597  cantnflem1  9598  epfrs  9640  dfac9  10047  axdc3lem4  10363  intwun  10646  r1limwun  10647  gruina  10729  grur1a  10730  mulclpi  10804  indpi  10818  supsrlem  11022  axpre-sup  11080  supfirege  12129  uzn0  12768  suprzub  12852  fzn0  13454  flval3  13735  icopnfsup  13785  hashelne0d  14291  dfrtrcl2  14985  01sqrexlem3  15167  isercolllem2  15589  isercolllem3  15590  climsup  15593  mertenslem2  15808  gcdcllem1  16426  pclem  16766  prmreclem1  16844  4sqlem13  16885  vdwmc2  16907  vdwlem6  16914  vdwnnlem3  16925  prmgaplem3  16981  prmgaplem4  16982  mrcflem  17529  mrcval  17533  iscatd2  17604  chnub  18545  mndbn0  18675  grpbn0  18896  issubgrpd2  19072  issubg4  19075  subgint  19080  nmzsubg  19094  cycsubgcl  19135  ghmpreima  19167  gastacl  19238  sylow1lem5  19531  pgpssslw  19543  sylow2alem2  19547  sylow2blem3  19551  fislw  19554  sylow3lem4  19559  torsubg  19783  oddvdssubg  19784  iscygd  19816  iscygodd  19817  dprdsubg  19955  ablfac1eu  20004  simpgnideld  20030  submomnd  20061  01eq0ring  20463  cntzsubrng  20500  cntzsubr  20539  imadrhmcl  20730  primefld  20738  primefld0cl  20739  primefld1cl  20740  abvn0b  20769  suborng  20809  islss4  20913  lss1d  20914  lssintcl  20915  lspsolvlem  21097  lbsextlem1  21113  dflidl2rng  21173  lidlsubg  21178  rhmpreimaidl  21232  zringlpirlem1  21417  ocvlss  21627  lmiclbs  21792  lmisfree  21797  psrbas  21889  mplsubglem  21954  mplind  22025  mhpsubg  22096  mat1ric  22431  dmatsgrp  22443  scmatsgrp  22463  scmatsgrp1  22466  scmatlss  22469  scmatric  22481  cpmatsubgpmat  22664  matcpmric  22703  pmmpric  22767  clscld  22991  2ndcdisj  23400  dfac14lem  23561  opnfbas  23786  isfil2  23800  filn0  23806  filssufilg  23855  rnelfmlem  23896  flimfnfcls  23972  ptcmplem2  23997  clssubg  24053  tgpconncomp  24057  tsmsfbas  24072  ustfilxp  24157  ustne0  24158  xbln0  24358  bln0  24359  metustfbas  24501  metustbl  24510  nrgdomn  24615  icccmplem2  24768  icccmplem3  24769  reconnlem2  24772  phtpcer  24950  reparpht  24954  phtpcco2  24955  pcohtpy  24976  pcorevlem  24982  isclmp  25053  iscmet3lem2  25248  bcthlem4  25283  minveclem3b  25384  ivthlem2  25409  ivthlem3  25410  evthicc  25416  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun2  25463  ioombl1lem4  25518  uniioombllem1  25538  uniioombllem2  25540  uniioombllem6  25545  mbfsup  25621  mbfinf  25622  mbflimsup  25623  itg2monolem1  25707  itg2mono  25710  ulm0  26356  pilem2  26418  pilem3  26419  ftalem3  27041  ftalem4  27042  ftalem5  27043  dchrabs  27227  pntlem3  27576  nocvxminlem  27750  bdayfinbndlem1  28463  tglnne0  28712  axlowdim1  29032  nvo00  30836  nmorepnf  30843  minvecolem1  30949  wrdpmtrlast  33175  cycpmco2lem5  33212  elrgspnlem1  33324  primefldchr  33383  fldgensdrg  33396  nsgqusf1olem1  33494  intlidl  33501  idlinsubrg  33512  rhmimaidl  33513  ssdifidl  33538  ssdifidlprm  33539  ssmxidl  33555  pidufd  33624  1arithufdlem1  33625  ply1dg1rtn0  33662  ply1degltlss  33677  exsslsb  33753  constrsdrg  33932  ordtconnlem1  34081  rrhre  34178  sigagenval  34297  oddpwdc  34511  bnj1177  35162  bnj1523  35227  rankfilimbi  35257  erdszelem8  35392  txsconnlem  35434  cvxsconn  35437  cvmsss2  35468  cvmliftmolem2  35476  cvmlift2lem12  35508  cvmliftpht  35512  finminlem  36512  onint1  36643  weiunlem  36657  weiunfr  36661  finxpreclem4  37599  heicant  37856  itg2addnc  37875  ftc1anclem7  37900  ftc1anc  37902  prdsbnd2  37996  lkrlss  39355  pclvalN  40150  dian0  41299  docaclN  41384  dicn0  41452  dihglblem5  41558  dihglb2  41602  doch2val2  41624  dochocss  41626  lclkr  41793  lclkrs  41799  lcfr  41845  aks6d1c6lem3  42426  unitscyglem2  42450  qsalrel  42496  nacsfix  42954  mzpcln0  42970  rencldnfilem  43062  fnwe2lem2  43293  kelac1  43305  harn0  43344  hbtlem2  43366  naddwordnexlem4  43643  omltoe  43648  gneispa  44371  imo72b2lem0  44406  scottrankd  44489  relpfrlem  45194  ubelsupr  45265  suprnmpt  45418  disjinfi  45436  suprubrnmpt2  45496  suprubrnmpt  45497  ssfiunibd  45557  allbutfi  45637  allbutfiinf  45664  uzn0d  45669  uzublem  45674  climinf  45852  limclr  45899  climinf2lem  45950  limsupubuzlem  45956  liminflelimsupuz  46029  cnrefiisplem  46073  ioodvbdlimc1lem1  46175  ioodvbdlimc1  46177  ioodvbdlimc2  46179  stoweidlem36  46280  fourierdlem20  46371  fourierdlem25  46376  fourierdlem31  46382  fourierdlem37  46388  fourierdlem46  46396  fourierdlem52  46402  fourierdlem54  46404  fouriercn  46476  elaa2lem  46477  salgenval  46565  salgenn0  46575  sge0isum  46671  sge0reuzb  46692  ovnlerp  46806  ovnf  46807  hsphoidmvle2  46829  hsphoidmvle  46830  hoiprodp1  46832  hoidmv1lelem1  46835  hoidmv1lelem3  46837  hoidmv1le  46838  hoidifhspdmvle  46864  hspmbllem1  46870  hspmbllem3  46872  ovnovollem2  46901  smflimlem1  47015  smfsuplem1  47055  smfsuplem3  47057  smflimsuplem5  47068  smflimsuplem7  47070  preimafvn0  47626  lincolss  48680  fvconstr2  49109  catprs  49256  discsubc  49309  iinfconstbas  49311  eloppf  49378  eloppf2  49379  oppcup3  49454  oppcthinendcALT  49686  termcterm3  49760  termcciso  49761  idfudiag1bas  49769  idfudiag1  49770