Theorem ne0d 4298

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2961  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-dif 3911  df-nul 4290

This theorem is used by:  snnzg  4745  prnzg  4749  eqsnd  4801  exss  5449  isofrlem  7349  peano3  7896  fvmpocurryd  8276  onnseq  8340  oeoalem  8591  oeoelem  8593  oeeui  8597  nnawordex  8632  omxpenlem  9076  frfi  9255  supgtoreq  9441  infltoreq  9474  cantnfp1lem2  9658  cantnfp1lem3  9659  oemapvali  9663  cantnflem1a  9664  cantnflem1d  9667  cantnflem1  9668  epfrs  9710  scottrankd  9888  dfac9  10139  axdc3lem4  10455  intwun  10738  r1limwun  10739  gruina  10821  grur1a  10822  mulclpi  10896  indpi  10910  supsrlem  11114  axpre-sup  11172  supfirege  12220  uzn0  12897  suprzub  12981  fzn0  13584  flval3  13868  icopnfsup  13918  hashelne0d  14424  dfrtrcl2  15125  01sqrexlem3  15321  isercolllem2  15743  isercolllem3  15744  climsup  15747  mertenslem2  15965  gcdcllem1  16582  pclem  16923  prmreclem1  17001  4sqlem13  17042  vdwmc2  17064  vdwlem6  17071  vdwnnlem3  17082  prmgaplem3  17138  prmgaplem4  17139  mrcflem  17687  mrcval  17691  iscatd2  17762  chnub  18703  mndbn0  18837  grpbn0  19064  issubgrpd2  19240  issubg4  19243  subgint  19248  nmzsubg  19262  cycsubgcl  19308  ghmpreima  19339  gastacl  19410  sylow1lem5  19703  pgpssslw  19715  sylow2alem2  19719  sylow2blem3  19723  fislw  19726  sylow3lem4  19731  torsubg  19955  oddvdssubg  19956  iscygd  19988  iscygodd  19989  dprdsubg  20127  ablfac1eu  20176  simpgnideld  20202  submomnd  20233  01eq0ring  20665  cntzsubrng  20703  cntzsubr  20742  imadrhmcl  20937  primefld  20945  primefld0cl  20946  primefld1cl  20947  abvn0b  20976  suborng  21016  islss4  21120  lss1d  21121  lssintcl  21122  lspsolvlem  21303  lbsextlem1  21319  dflidl2rng  21380  lidlsubg  21385  lidlunin0  21398  rhmpreimaidl  21453  ssdifidl  21522  ssdifidlprm  21523  zringlpirlem1  21649  ocvlss  21859  lmiclbs  22024  lmisfree  22029  psrbas  22121  mplsubglem  22185  mplind  22258  mhpsubg  22353  mat1ric  22681  dmatsgrp  22693  scmatsgrp  22713  scmatsgrp1  22716  scmatlss  22719  scmatric  22731  cpmatsubgpmat  22914  matcpmric  22953  pmmpric  23017  clscld  23241  2ndcdisj  23650  dfac14lem  23811  opnfbas  24036  isfil2  24050  filn0  24056  filssufilg  24105  rnelfmlem  24146  flimfnfcls  24222  ptcmplem2  24247  clssubg  24303  tgpconncomp  24307  tsmsfbas  24322  ustfilxp  24407  ustne0  24408  xbln0  24608  bln0  24609  metustfbas  24751  metustbl  24760  nrgdomn  24865  icccmplem2  25018  icccmplem3  25019  reconnlem2  25022  phtpcer  25191  reparpht  25194  phtpcco2  25195  pcohtpy  25216  pcorevlem  25222  isclmp  25293  iscmet3lem2  25488  bcthlem4  25523  minveclem3b  25624  ivthlem2  25648  ivthlem3  25649  evthicc  25655  ovollb2  25685  ovolunlem1a  25692  ovolunlem1  25693  ovoliunlem1  25698  ovoliun2  25702  ioombl1lem4  25757  uniioombllem1  25777  uniioombllem2  25779  uniioombllem6  25784  mbfsup  25860  mbfinf  25861  mbflimsup  25862  itg2monolem1  25946  itg2mono  25949  ulm0  26591  pilem2  26652  pilem3  26653  ftalem3  27276  ftalem4  27277  ftalem5  27278  dchrabs  27461  pntlem3  27810  nocvxminlem  27984  bdayfinbndlem1  28697  tglnne0  28951  tglnpt4  28965  prlngmolem1  29239  prlngmolem2  29240  prlngmo2  29243  prlngpln4  29245  prlngsymquadlem  29250  quadcgrprlng  29253  axlowdim1  29346  nvo00  31150  nmorepnf  31157  minvecolem1  31263  wrdpmtrlast  33444  cycpmco2lem5  33481  elrgspnlem1  33593  primefldchr  33653  fldgensdrg  33666  nsgqusf1olem1  33753  intlidl  33759  idlinsubrg  33770  rhmimaidl  33771  ssmxidl  33788  dflringlem2  33816  pidufd  33864  1arithufdlem1  33865  ply1dg1rtn0  33902  ply1degltlss  33917  exsslsb  34018  constrsdrg  34196  ordtconnlem1  34345  rrhre  34442  sigagenval  34562  oddpwdc  34776  bnj1177  35426  bnj1523  35491  rankfilimbi  35520  erdszelem8  35711  txsconnlem  35753  cvxsconn  35756  cvmsss2  35787  cvmliftmolem2  35795  cvmlift2lem12  35827  cvmliftpht  35831  finminlem  36870  onint1  37001  weiunlem  37015  weiunfr  37019  finxpreclem4  38081  heicant  38347  itg2addnc  38366  ftc1anclem7  38391  ftc1anc  38393  prdsbnd2  38487  lkrlss  39910  pclvalN  40705  dian0  41854  docaclN  41939  dicn0  42007  dihglblem5  42113  dihglb2  42157  doch2val2  42179  dochocss  42181  lclkr  42348  lclkrs  42354  lcfr  42400  aks6d1c6lem3  42980  unitscyglem2  43004  qsalrel  43050  nacsfix  43484  mzpcln0  43500  rencldnfilem  43588  fnwe2lem2  43819  kelac1  43831  harn0  43870  hbtlem2  43892  naddwordnexlem4  44169  omltoe  44174  gneispa  44897  imo72b2lem0  44932  relpfrlem  45703  ubelsupr  45781  suprnmpt  45933  disjinfi  45951  suprubrnmpt2  46008  suprubrnmpt  46009  ssfiunibd  46069  allbutfi  46149  allbutfiinf  46175  uzn0d  46180  uzublem  46185  climinf  46363  limclr  46410  climinf2lem  46461  limsupubuzlem  46467  liminflelimsupuz  46540  cnrefiisplem  46584  ioodvbdlimc1lem1  46686  ioodvbdlimc1  46688  ioodvbdlimc2  46690  stoweidlem36  46791  fourierdlem20  46882  fourierdlem25  46887  fourierdlem31  46893  fourierdlem37  46899  fourierdlem46  46907  fourierdlem48  46909  fourierdlem49  46910  fourierdlem52  46913  fourierdlem54  46915  fouriercn  46987  elaa2lem  46988  salgenval  47076  salgenn0  47086  sge0isum  47182  sge0reuzb  47203  ovnlerp  47317  ovnf  47318  hsphoidmvle2  47340  hsphoidmvle  47341  hoiprodp1  47343  hoidmv1lelem1  47346  hoidmv1lelem3  47348  hoidmv1le  47349  hoidifhspdmvle  47375  hspmbllem1  47381  hspmbllem3  47383  ovnovollem2  47412  smflimlem1  47526  smfsuplem1  47566  smfsuplem3  47568  smflimsuplem5  47579  smflimsuplem7  47581  preimafvn0  48170  lincolss  49255  fvconstr2  49683  catprs  49830  discsubc  49883  iinfconstbas  49885  eloppf  49952  eloppf2  49953  oppcup3  50028  oppcthinendcALT  50260  termcterm3  50334  termcciso  50335  idfudiag1bas  50343  idfudiag1  50344