Theorem ne0d 4266

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-dif 3886  df-nul 4254

This theorem is referenced by:  snnzg  4707  prnzg  4711  exss  5372  isofrlem  7191  fvmpocurryd  8058  onnseq  8146  oeoalem  8389  oeoelem  8391  oeeui  8395  nnawordex  8430  omxpenlem  8813  frfi  8989  supgtoreq  9159  infltoreq  9191  cantnfp1lem2  9367  cantnfp1lem3  9368  oemapvali  9372  cantnflem1a  9373  cantnflem1d  9376  cantnflem1  9377  epfrs  9420  dfac9  9823  axdc3lem4  10140  intwun  10422  r1limwun  10423  gruina  10505  grur1a  10506  mulclpi  10580  indpi  10594  supsrlem  10798  axpre-sup  10856  supfirege  11892  uzn0  12528  suprzub  12608  fzn0  13199  flval3  13463  icopnfsup  13513  hashelne0d  14011  dfrtrcl2  14701  sqrlem3  14884  isercolllem2  15305  isercolllem3  15306  climsup  15309  mertenslem2  15525  gcdcllem1  16134  pclem  16467  prmreclem1  16545  4sqlem13  16586  vdwmc2  16608  vdwlem6  16615  vdwnnlem3  16626  prmgaplem3  16682  prmgaplem4  16683  mrcflem  17232  mrcval  17236  iscatd2  17307  mndbn0  18316  grpbn0  18523  issubgrpd2  18686  issubg4  18689  subgint  18694  nmzsubg  18708  cycsubgcl  18740  ghmpreima  18771  gastacl  18830  sylow1lem5  19122  pgpssslw  19134  sylow2alem2  19138  sylow2blem3  19142  fislw  19145  sylow3lem4  19150  torsubg  19370  oddvdssubg  19371  iscygd  19402  iscygodd  19403  dprdsubg  19542  ablfac1eu  19591  simpgnideld  19617  cntzsubr  19972  primefld  19988  primefld0cl  19989  primefld1cl  19990  islss4  20139  lss1d  20140  lssintcl  20141  lspsolvlem  20319  lbsextlem1  20335  lidlsubg  20399  abvn0b  20486  zringlpirlem1  20596  ocvlss  20789  lmiclbs  20954  lmisfree  20959  psrbas  21057  mplsubglem  21115  mplind  21188  mhpsubg  21253  mat1ric  21544  dmatsgrp  21556  scmatsgrp  21576  scmatsgrp1  21579  scmatlss  21582  scmatric  21594  cpmatsubgpmat  21777  matcpmric  21816  pmmpric  21880  clscld  22106  2ndcdisj  22515  dfac14lem  22676  opnfbas  22901  isfil2  22915  filn0  22921  filssufilg  22970  rnelfmlem  23011  flimfnfcls  23087  ptcmplem2  23112  clssubg  23168  tgpconncomp  23172  tsmsfbas  23187  ustfilxp  23272  ustne0  23273  xbln0  23475  bln0  23476  metustfbas  23619  metustbl  23628  nrgdomn  23741  icccmplem2  23892  icccmplem3  23893  reconnlem2  23896  phtpcer  24064  reparpht  24067  phtpcco2  24068  pcohtpy  24089  pcorevlem  24095  isclmp  24166  iscmet3lem2  24361  bcthlem4  24396  minveclem3b  24497  ivthlem2  24521  ivthlem3  24522  evthicc  24528  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliun2  24575  ioombl1lem4  24630  uniioombllem1  24650  uniioombllem2  24652  uniioombllem6  24657  mbfsup  24733  mbfinf  24734  mbflimsup  24735  itg2monolem1  24820  itg2mono  24823  ulm0  25455  pilem2  25516  pilem3  25517  ftalem3  26129  ftalem4  26130  ftalem5  26131  dchrabs  26313  pntlem3  26662  tglnne0  26905  axlowdim1  27230  nvo00  29024  nmorepnf  29031  minvecolem1  29137  submomnd  31238  cycpmco2lem5  31299  primefldchr  31395  suborng  31416  nsgqusf1olem1  31500  intlidl  31504  rhmpreimaidl  31505  idlinsubrg  31510  rhmimaidl  31511  ssmxidl  31544  ordtconnlem1  31776  rrhre  31871  sigagenval  32008  oddpwdc  32221  bnj1177  32886  bnj1523  32951  erdszelem8  33060  txsconnlem  33102  cvxsconn  33105  cvmsss2  33136  cvmliftmolem2  33144  cvmlift2lem12  33176  cvmliftpht  33180  nocvxminlem  33899  finminlem  34434  onint1  34565  finxpreclem4  35492  heicant  35739  itg2addnc  35758  ftc1anclem7  35783  ftc1anc  35785  prdsbnd2  35880  lkrlss  37036  pclvalN  37831  dian0  38980  docaclN  39065  dicn0  39133  dihglblem5  39239  dihglb2  39283  doch2val2  39305  dochocss  39307  lclkr  39474  lclkrs  39480  lcfr  39526  qsalrel  40141  nacsfix  40450  mzpcln0  40466  rencldnfilem  40558  fnwe2lem2  40792  kelac1  40804  harn0  40843  hbtlem2  40865  gneispa  41629  scottrankd  41755  ubelsupr  42452  suprnmpt  42599  disjinfi  42620  suprubrnmpt2  42687  suprubrnmpt  42688  ssfiunibd  42738  allbutfi  42823  allbutfiinf  42850  uzn0d  42855  uzublem  42860  climinf  43037  limclr  43086  climinf2lem  43137  limsupubuzlem  43143  liminflelimsupuz  43216  cnrefiisplem  43260  ioodvbdlimc1lem1  43362  ioodvbdlimc1  43364  ioodvbdlimc2  43366  stoweidlem36  43467  fourierdlem20  43558  fourierdlem25  43563  fourierdlem31  43569  fourierdlem37  43575  fourierdlem46  43583  fourierdlem52  43589  fourierdlem54  43591  fouriercn  43663  elaa2lem  43664  salgenval  43752  salgenn0  43760  sge0isum  43855  sge0reuzb  43876  ovnlerp  43990  ovnf  43991  hsphoidmvle2  44013  hsphoidmvle  44014  hoiprodp1  44016  hoidmv1lelem1  44019  hoidmv1lelem3  44021  hoidmv1le  44022  hoidifhspdmvle  44048  hspmbllem1  44054  hspmbllem3  44056  ovnovollem2  44085  smflimlem1  44193  smfsuplem1  44231  smfsuplem3  44233  smflimsuplem5  44244  smflimsuplem7  44246  preimafvn0  44720  lincolss  45663  fvconstr2  46073  catprs  46180