Theorem ne0d 4317

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-dif 3929  df-nul 4309

This theorem is referenced by:  snnzg  4750  prnzg  4754  eqsnd  4806  exss  5438  isofrlem  7332  fvmpocurryd  8268  onnseq  8356  oeoalem  8606  oeoelem  8608  oeeui  8612  nnawordex  8647  omxpenlem  9085  frfi  9291  supgtoreq  9481  infltoreq  9514  cantnfp1lem2  9691  cantnfp1lem3  9692  oemapvali  9696  cantnflem1a  9697  cantnflem1d  9700  cantnflem1  9701  epfrs  9743  dfac9  10149  axdc3lem4  10465  intwun  10747  r1limwun  10748  gruina  10830  grur1a  10831  mulclpi  10905  indpi  10919  supsrlem  11123  axpre-sup  11181  supfirege  12227  uzn0  12867  suprzub  12953  fzn0  13553  flval3  13830  icopnfsup  13880  hashelne0d  14384  dfrtrcl2  15079  01sqrexlem3  15261  isercolllem2  15680  isercolllem3  15681  climsup  15684  mertenslem2  15899  gcdcllem1  16516  pclem  16856  prmreclem1  16934  4sqlem13  16975  vdwmc2  16997  vdwlem6  17004  vdwnnlem3  17015  prmgaplem3  17071  prmgaplem4  17072  mrcflem  17616  mrcval  17620  iscatd2  17691  mndbn0  18726  grpbn0  18947  issubgrpd2  19123  issubg4  19126  subgint  19131  nmzsubg  19146  cycsubgcl  19187  ghmpreima  19219  gastacl  19290  sylow1lem5  19581  pgpssslw  19593  sylow2alem2  19597  sylow2blem3  19601  fislw  19604  sylow3lem4  19609  torsubg  19833  oddvdssubg  19834  iscygd  19866  iscygodd  19867  dprdsubg  20005  ablfac1eu  20054  simpgnideld  20080  01eq0ring  20488  cntzsubrng  20525  cntzsubr  20564  imadrhmcl  20755  primefld  20763  primefld0cl  20764  primefld1cl  20765  abvn0b  20794  islss4  20917  lss1d  20918  lssintcl  20919  lspsolvlem  21101  lbsextlem1  21117  dflidl2rng  21177  lidlsubg  21182  rhmpreimaidl  21236  zringlpirlem1  21421  ocvlss  21630  lmiclbs  21795  lmisfree  21800  psrbas  21891  mplsubglem  21957  mplind  22026  mhpsubg  22089  mat1ric  22423  dmatsgrp  22435  scmatsgrp  22455  scmatsgrp1  22458  scmatlss  22461  scmatric  22473  cpmatsubgpmat  22656  matcpmric  22695  pmmpric  22759  clscld  22983  2ndcdisj  23392  dfac14lem  23553  opnfbas  23778  isfil2  23792  filn0  23798  filssufilg  23847  rnelfmlem  23888  flimfnfcls  23964  ptcmplem2  23989  clssubg  24045  tgpconncomp  24049  tsmsfbas  24064  ustfilxp  24149  ustne0  24150  xbln0  24351  bln0  24352  metustfbas  24494  metustbl  24503  nrgdomn  24608  icccmplem2  24761  icccmplem3  24762  reconnlem2  24765  phtpcer  24943  reparpht  24947  phtpcco2  24948  pcohtpy  24969  pcorevlem  24975  isclmp  25046  iscmet3lem2  25242  bcthlem4  25277  minveclem3b  25378  ivthlem2  25403  ivthlem3  25404  evthicc  25410  ovollb2  25440  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliun2  25457  ioombl1lem4  25512  uniioombllem1  25532  uniioombllem2  25534  uniioombllem6  25539  mbfsup  25615  mbfinf  25616  mbflimsup  25617  itg2monolem1  25701  itg2mono  25704  ulm0  26350  pilem2  26412  pilem3  26413  ftalem3  27035  ftalem4  27036  ftalem5  27037  dchrabs  27221  pntlem3  27570  nocvxminlem  27739  tglnne0  28565  axlowdim1  28884  nvo00  30688  nmorepnf  30695  minvecolem1  30801  chnub  32938  submomnd  33024  wrdpmtrlast  33050  cycpmco2lem5  33087  elrgspnlem1  33183  primefldchr  33241  fldgensdrg  33254  suborng  33283  nsgqusf1olem1  33374  intlidl  33381  idlinsubrg  33392  rhmimaidl  33393  ssdifidl  33418  ssdifidlprm  33419  ssmxidl  33435  pidufd  33504  1arithufdlem1  33505  ply1dg1rtn0  33539  ply1degltlss  33552  exsslsb  33582  constrsdrg  33755  ordtconnlem1  33901  rrhre  33998  sigagenval  34117  oddpwdc  34332  bnj1177  34983  bnj1523  35048  erdszelem8  35166  txsconnlem  35208  cvxsconn  35211  cvmsss2  35242  cvmliftmolem2  35250  cvmlift2lem12  35282  cvmliftpht  35286  finminlem  36282  onint1  36413  weiunlem2  36427  weiunfr  36431  finxpreclem4  37358  heicant  37625  itg2addnc  37644  ftc1anclem7  37669  ftc1anc  37671  prdsbnd2  37765  lkrlss  39059  pclvalN  39855  dian0  41004  docaclN  41089  dicn0  41157  dihglblem5  41263  dihglb2  41307  doch2val2  41329  dochocss  41331  lclkr  41498  lclkrs  41504  lcfr  41550  aks6d1c6lem3  42131  unitscyglem2  42155  qsalrel  42238  nacsfix  42682  mzpcln0  42698  rencldnfilem  42790  fnwe2lem2  43022  kelac1  43034  harn0  43073  hbtlem2  43095  naddwordnexlem4  43372  omltoe  43378  gneispa  44101  imo72b2lem0  44136  scottrankd  44220  relpfrlem  44926  ubelsupr  44992  suprnmpt  45146  disjinfi  45164  suprubrnmpt2  45224  suprubrnmpt  45225  ssfiunibd  45286  allbutfi  45368  allbutfiinf  45395  uzn0d  45400  uzublem  45405  climinf  45583  limclr  45632  climinf2lem  45683  limsupubuzlem  45689  liminflelimsupuz  45762  cnrefiisplem  45806  ioodvbdlimc1lem1  45908  ioodvbdlimc1  45910  ioodvbdlimc2  45912  stoweidlem36  46013  fourierdlem20  46104  fourierdlem25  46109  fourierdlem31  46115  fourierdlem37  46121  fourierdlem46  46129  fourierdlem52  46135  fourierdlem54  46137  fouriercn  46209  elaa2lem  46210  salgenval  46298  salgenn0  46308  sge0isum  46404  sge0reuzb  46425  ovnlerp  46539  ovnf  46540  hsphoidmvle2  46562  hsphoidmvle  46563  hoiprodp1  46565  hoidmv1lelem1  46568  hoidmv1lelem3  46570  hoidmv1le  46571  hoidifhspdmvle  46597  hspmbllem1  46603  hspmbllem3  46605  ovnovollem2  46634  smflimlem1  46748  smfsuplem1  46788  smfsuplem3  46790  smflimsuplem5  46801  smflimsuplem7  46803  preimafvn0  47342  lincolss  48358  fvconstr2  48788  catprs  48934  discsubc  48979  iinfconstbas  48981  oppcup3  49090  oppcthinendcALT  49275  termcterm3  49348  termcciso  49349  idfudiag1bas  49357  idfudiag1  49358