Theorem ne0d 4305

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ∅c0 4296

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3917  df-nul 4297

This theorem is referenced by:  snnzg  4738  prnzg  4742  eqsnd  4794  exss  5423  isofrlem  7315  fvmpocurryd  8250  onnseq  8313  oeoalem  8560  oeoelem  8562  oeeui  8566  nnawordex  8601  omxpenlem  9042  frfi  9232  supgtoreq  9422  infltoreq  9455  cantnfp1lem2  9632  cantnfp1lem3  9633  oemapvali  9637  cantnflem1a  9638  cantnflem1d  9641  cantnflem1  9642  epfrs  9684  dfac9  10090  axdc3lem4  10406  intwun  10688  r1limwun  10689  gruina  10771  grur1a  10772  mulclpi  10846  indpi  10860  supsrlem  11064  axpre-sup  11122  supfirege  12170  uzn0  12810  suprzub  12898  fzn0  13499  flval3  13777  icopnfsup  13827  hashelne0d  14333  dfrtrcl2  15028  01sqrexlem3  15210  isercolllem2  15632  isercolllem3  15633  climsup  15636  mertenslem2  15851  gcdcllem1  16469  pclem  16809  prmreclem1  16887  4sqlem13  16928  vdwmc2  16950  vdwlem6  16957  vdwnnlem3  16968  prmgaplem3  17024  prmgaplem4  17025  mrcflem  17567  mrcval  17571  iscatd2  17642  mndbn0  18677  grpbn0  18898  issubgrpd2  19074  issubg4  19077  subgint  19082  nmzsubg  19097  cycsubgcl  19138  ghmpreima  19170  gastacl  19241  sylow1lem5  19532  pgpssslw  19544  sylow2alem2  19548  sylow2blem3  19552  fislw  19555  sylow3lem4  19560  torsubg  19784  oddvdssubg  19785  iscygd  19817  iscygodd  19818  dprdsubg  19956  ablfac1eu  20005  simpgnideld  20031  01eq0ring  20439  cntzsubrng  20476  cntzsubr  20515  imadrhmcl  20706  primefld  20714  primefld0cl  20715  primefld1cl  20716  abvn0b  20745  islss4  20868  lss1d  20869  lssintcl  20870  lspsolvlem  21052  lbsextlem1  21068  dflidl2rng  21128  lidlsubg  21133  rhmpreimaidl  21187  zringlpirlem1  21372  ocvlss  21581  lmiclbs  21746  lmisfree  21751  psrbas  21842  mplsubglem  21908  mplind  21977  mhpsubg  22040  mat1ric  22374  dmatsgrp  22386  scmatsgrp  22406  scmatsgrp1  22409  scmatlss  22412  scmatric  22424  cpmatsubgpmat  22607  matcpmric  22646  pmmpric  22710  clscld  22934  2ndcdisj  23343  dfac14lem  23504  opnfbas  23729  isfil2  23743  filn0  23749  filssufilg  23798  rnelfmlem  23839  flimfnfcls  23915  ptcmplem2  23940  clssubg  23996  tgpconncomp  24000  tsmsfbas  24015  ustfilxp  24100  ustne0  24101  xbln0  24302  bln0  24303  metustfbas  24445  metustbl  24454  nrgdomn  24559  icccmplem2  24712  icccmplem3  24713  reconnlem2  24716  phtpcer  24894  reparpht  24898  phtpcco2  24899  pcohtpy  24920  pcorevlem  24926  isclmp  24997  iscmet3lem2  25192  bcthlem4  25227  minveclem3b  25328  ivthlem2  25353  ivthlem3  25354  evthicc  25360  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun2  25407  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem2  25484  uniioombllem6  25489  mbfsup  25565  mbfinf  25566  mbflimsup  25567  itg2monolem1  25651  itg2mono  25654  ulm0  26300  pilem2  26362  pilem3  26363  ftalem3  26985  ftalem4  26986  ftalem5  26987  dchrabs  27171  pntlem3  27520  nocvxminlem  27689  tglnne0  28567  axlowdim1  28886  nvo00  30690  nmorepnf  30697  minvecolem1  30803  chnub  32938  submomnd  33024  wrdpmtrlast  33050  cycpmco2lem5  33087  elrgspnlem1  33193  primefldchr  33251  fldgensdrg  33264  suborng  33293  nsgqusf1olem1  33384  intlidl  33391  idlinsubrg  33402  rhmimaidl  33403  ssdifidl  33428  ssdifidlprm  33429  ssmxidl  33445  pidufd  33514  1arithufdlem1  33515  ply1dg1rtn0  33549  ply1degltlss  33562  exsslsb  33592  constrsdrg  33765  ordtconnlem1  33914  rrhre  34011  sigagenval  34130  oddpwdc  34345  bnj1177  34996  bnj1523  35061  erdszelem8  35185  txsconnlem  35227  cvxsconn  35230  cvmsss2  35261  cvmliftmolem2  35269  cvmlift2lem12  35301  cvmliftpht  35305  finminlem  36306  onint1  36437  weiunlem2  36451  weiunfr  36455  finxpreclem4  37382  heicant  37649  itg2addnc  37668  ftc1anclem7  37693  ftc1anc  37695  prdsbnd2  37789  lkrlss  39088  pclvalN  39884  dian0  41033  docaclN  41118  dicn0  41186  dihglblem5  41292  dihglb2  41336  doch2val2  41358  dochocss  41360  lclkr  41527  lclkrs  41533  lcfr  41579  aks6d1c6lem3  42160  unitscyglem2  42184  qsalrel  42228  nacsfix  42700  mzpcln0  42716  rencldnfilem  42808  fnwe2lem2  43040  kelac1  43052  harn0  43091  hbtlem2  43113  naddwordnexlem4  43390  omltoe  43396  gneispa  44119  imo72b2lem0  44154  scottrankd  44237  relpfrlem  44943  ubelsupr  45014  suprnmpt  45168  disjinfi  45186  suprubrnmpt2  45246  suprubrnmpt  45247  ssfiunibd  45307  allbutfi  45389  allbutfiinf  45416  uzn0d  45421  uzublem  45426  climinf  45604  limclr  45653  climinf2lem  45704  limsupubuzlem  45710  liminflelimsupuz  45783  cnrefiisplem  45827  ioodvbdlimc1lem1  45929  ioodvbdlimc1  45931  ioodvbdlimc2  45933  stoweidlem36  46034  fourierdlem20  46125  fourierdlem25  46130  fourierdlem31  46136  fourierdlem37  46142  fourierdlem46  46150  fourierdlem52  46156  fourierdlem54  46158  fouriercn  46230  elaa2lem  46231  salgenval  46319  salgenn0  46329  sge0isum  46425  sge0reuzb  46446  ovnlerp  46560  ovnf  46561  hsphoidmvle2  46583  hsphoidmvle  46584  hoiprodp1  46586  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmv1le  46592  hoidifhspdmvle  46618  hspmbllem1  46624  hspmbllem3  46626  ovnovollem2  46655  smflimlem1  46769  smfsuplem1  46809  smfsuplem3  46811  smflimsuplem5  46822  smflimsuplem7  46824  preimafvn0  47381  lincolss  48423  fvconstr2  48852  catprs  49000  discsubc  49053  iinfconstbas  49055  eloppf  49122  eloppf2  49123  oppcup3  49198  oppcthinendcALT  49430  termcterm3  49504  termcciso  49505  idfudiag1bas  49513  idfudiag1  49514