Theorem ne0d 4295

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

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

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 3908  df-nul 4287

This theorem is referenced by:  snnzg  4728  prnzg  4732  eqsnd  4784  exss  5410  isofrlem  7281  fvmpocurryd  8211  onnseq  8274  oeoalem  8521  oeoelem  8523  oeeui  8527  nnawordex  8562  omxpenlem  9002  frfi  9190  supgtoreq  9380  infltoreq  9413  cantnfp1lem2  9594  cantnfp1lem3  9595  oemapvali  9599  cantnflem1a  9600  cantnflem1d  9603  cantnflem1  9604  epfrs  9646  dfac9  10050  axdc3lem4  10366  intwun  10648  r1limwun  10649  gruina  10731  grur1a  10732  mulclpi  10806  indpi  10820  supsrlem  11024  axpre-sup  11082  supfirege  12130  uzn0  12770  suprzub  12858  fzn0  13459  flval3  13737  icopnfsup  13787  hashelne0d  14293  dfrtrcl2  14987  01sqrexlem3  15169  isercolllem2  15591  isercolllem3  15592  climsup  15595  mertenslem2  15810  gcdcllem1  16428  pclem  16768  prmreclem1  16846  4sqlem13  16887  vdwmc2  16909  vdwlem6  16916  vdwnnlem3  16927  prmgaplem3  16983  prmgaplem4  16984  mrcflem  17530  mrcval  17534  iscatd2  17605  mndbn0  18642  grpbn0  18863  issubgrpd2  19039  issubg4  19042  subgint  19047  nmzsubg  19062  cycsubgcl  19103  ghmpreima  19135  gastacl  19206  sylow1lem5  19499  pgpssslw  19511  sylow2alem2  19515  sylow2blem3  19519  fislw  19522  sylow3lem4  19527  torsubg  19751  oddvdssubg  19752  iscygd  19784  iscygodd  19785  dprdsubg  19923  ablfac1eu  19972  simpgnideld  19998  submomnd  20029  01eq0ring  20433  cntzsubrng  20470  cntzsubr  20509  imadrhmcl  20700  primefld  20708  primefld0cl  20709  primefld1cl  20710  abvn0b  20739  suborng  20779  islss4  20883  lss1d  20884  lssintcl  20885  lspsolvlem  21067  lbsextlem1  21083  dflidl2rng  21143  lidlsubg  21148  rhmpreimaidl  21202  zringlpirlem1  21387  ocvlss  21597  lmiclbs  21762  lmisfree  21767  psrbas  21858  mplsubglem  21924  mplind  21993  mhpsubg  22056  mat1ric  22390  dmatsgrp  22402  scmatsgrp  22422  scmatsgrp1  22425  scmatlss  22428  scmatric  22440  cpmatsubgpmat  22623  matcpmric  22662  pmmpric  22726  clscld  22950  2ndcdisj  23359  dfac14lem  23520  opnfbas  23745  isfil2  23759  filn0  23765  filssufilg  23814  rnelfmlem  23855  flimfnfcls  23931  ptcmplem2  23956  clssubg  24012  tgpconncomp  24016  tsmsfbas  24031  ustfilxp  24116  ustne0  24117  xbln0  24318  bln0  24319  metustfbas  24461  metustbl  24470  nrgdomn  24575  icccmplem2  24728  icccmplem3  24729  reconnlem2  24732  phtpcer  24910  reparpht  24914  phtpcco2  24915  pcohtpy  24936  pcorevlem  24942  isclmp  25013  iscmet3lem2  25208  bcthlem4  25243  minveclem3b  25344  ivthlem2  25369  ivthlem3  25370  evthicc  25376  ovollb2  25406  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliun2  25423  ioombl1lem4  25478  uniioombllem1  25498  uniioombllem2  25500  uniioombllem6  25505  mbfsup  25581  mbfinf  25582  mbflimsup  25583  itg2monolem1  25667  itg2mono  25670  ulm0  26316  pilem2  26378  pilem3  26379  ftalem3  27001  ftalem4  27002  ftalem5  27003  dchrabs  27187  pntlem3  27536  nocvxminlem  27706  tglnne0  28603  axlowdim1  28922  nvo00  30723  nmorepnf  30730  minvecolem1  30836  chnub  32967  wrdpmtrlast  33048  cycpmco2lem5  33085  elrgspnlem1  33195  primefldchr  33253  fldgensdrg  33266  nsgqusf1olem1  33363  intlidl  33370  idlinsubrg  33381  rhmimaidl  33382  ssdifidl  33407  ssdifidlprm  33408  ssmxidl  33424  pidufd  33493  1arithufdlem1  33494  ply1dg1rtn0  33528  ply1degltlss  33541  exsslsb  33571  constrsdrg  33744  ordtconnlem1  33893  rrhre  33990  sigagenval  34109  oddpwdc  34324  bnj1177  34975  bnj1523  35040  erdszelem8  35173  txsconnlem  35215  cvxsconn  35218  cvmsss2  35249  cvmliftmolem2  35257  cvmlift2lem12  35289  cvmliftpht  35293  finminlem  36294  onint1  36425  weiunlem2  36439  weiunfr  36443  finxpreclem4  37370  heicant  37637  itg2addnc  37656  ftc1anclem7  37681  ftc1anc  37683  prdsbnd2  37777  lkrlss  39076  pclvalN  39872  dian0  41021  docaclN  41106  dicn0  41174  dihglblem5  41280  dihglb2  41324  doch2val2  41346  dochocss  41348  lclkr  41515  lclkrs  41521  lcfr  41567  aks6d1c6lem3  42148  unitscyglem2  42172  qsalrel  42216  nacsfix  42688  mzpcln0  42704  rencldnfilem  42796  fnwe2lem2  43027  kelac1  43039  harn0  43078  hbtlem2  43100  naddwordnexlem4  43377  omltoe  43383  gneispa  44106  imo72b2lem0  44141  scottrankd  44224  relpfrlem  44930  ubelsupr  45001  suprnmpt  45155  disjinfi  45173  suprubrnmpt2  45233  suprubrnmpt  45234  ssfiunibd  45294  allbutfi  45376  allbutfiinf  45403  uzn0d  45408  uzublem  45413  climinf  45591  limclr  45640  climinf2lem  45691  limsupubuzlem  45697  liminflelimsupuz  45770  cnrefiisplem  45814  ioodvbdlimc1lem1  45916  ioodvbdlimc1  45918  ioodvbdlimc2  45920  stoweidlem36  46021  fourierdlem20  46112  fourierdlem25  46117  fourierdlem31  46123  fourierdlem37  46129  fourierdlem46  46137  fourierdlem52  46143  fourierdlem54  46145  fouriercn  46217  elaa2lem  46218  salgenval  46306  salgenn0  46316  sge0isum  46412  sge0reuzb  46433  ovnlerp  46547  ovnf  46548  hsphoidmvle2  46570  hsphoidmvle  46571  hoiprodp1  46573  hoidmv1lelem1  46576  hoidmv1lelem3  46578  hoidmv1le  46579  hoidifhspdmvle  46605  hspmbllem1  46611  hspmbllem3  46613  ovnovollem2  46642  smflimlem1  46756  smfsuplem1  46796  smfsuplem3  46798  smflimsuplem5  46809  smflimsuplem7  46811  preimafvn0  47368  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