Theorem ne0d 4296

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3906  df-nul 4288

This theorem is referenced by:  snnzg  4733  prnzg  4737  eqsnd  4788  exss  5418  isofrlem  7296  fvmpocurryd  8223  onnseq  8286  oeoalem  8534  oeoelem  8536  oeeui  8540  nnawordex  8575  omxpenlem  9018  frfi  9197  supgtoreq  9386  infltoreq  9419  cantnfp1lem2  9600  cantnfp1lem3  9601  oemapvali  9605  cantnflem1a  9606  cantnflem1d  9609  cantnflem1  9610  epfrs  9652  dfac9  10059  axdc3lem4  10375  intwun  10658  r1limwun  10659  gruina  10741  grur1a  10742  mulclpi  10816  indpi  10830  supsrlem  11034  axpre-sup  11092  supfirege  12141  uzn0  12780  suprzub  12864  fzn0  13466  flval3  13747  icopnfsup  13797  hashelne0d  14303  dfrtrcl2  14997  01sqrexlem3  15179  isercolllem2  15601  isercolllem3  15602  climsup  15605  mertenslem2  15820  gcdcllem1  16438  pclem  16778  prmreclem1  16856  4sqlem13  16897  vdwmc2  16919  vdwlem6  16926  vdwnnlem3  16937  prmgaplem3  16993  prmgaplem4  16994  mrcflem  17541  mrcval  17545  iscatd2  17616  chnub  18557  mndbn0  18687  grpbn0  18908  issubgrpd2  19084  issubg4  19087  subgint  19092  nmzsubg  19106  cycsubgcl  19147  ghmpreima  19179  gastacl  19250  sylow1lem5  19543  pgpssslw  19555  sylow2alem2  19559  sylow2blem3  19563  fislw  19566  sylow3lem4  19571  torsubg  19795  oddvdssubg  19796  iscygd  19828  iscygodd  19829  dprdsubg  19967  ablfac1eu  20016  simpgnideld  20042  submomnd  20073  01eq0ring  20475  cntzsubrng  20512  cntzsubr  20551  imadrhmcl  20742  primefld  20750  primefld0cl  20751  primefld1cl  20752  abvn0b  20781  suborng  20821  islss4  20925  lss1d  20926  lssintcl  20927  lspsolvlem  21109  lbsextlem1  21125  dflidl2rng  21185  lidlsubg  21190  rhmpreimaidl  21244  zringlpirlem1  21429  ocvlss  21639  lmiclbs  21804  lmisfree  21809  psrbas  21901  mplsubglem  21966  mplind  22037  mhpsubg  22108  mat1ric  22443  dmatsgrp  22455  scmatsgrp  22475  scmatsgrp1  22478  scmatlss  22481  scmatric  22493  cpmatsubgpmat  22676  matcpmric  22715  pmmpric  22779  clscld  23003  2ndcdisj  23412  dfac14lem  23573  opnfbas  23798  isfil2  23812  filn0  23818  filssufilg  23867  rnelfmlem  23908  flimfnfcls  23984  ptcmplem2  24009  clssubg  24065  tgpconncomp  24069  tsmsfbas  24084  ustfilxp  24169  ustne0  24170  xbln0  24370  bln0  24371  metustfbas  24513  metustbl  24522  nrgdomn  24627  icccmplem2  24780  icccmplem3  24781  reconnlem2  24784  phtpcer  24962  reparpht  24966  phtpcco2  24967  pcohtpy  24988  pcorevlem  24994  isclmp  25065  iscmet3lem2  25260  bcthlem4  25295  minveclem3b  25396  ivthlem2  25421  ivthlem3  25422  evthicc  25428  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun2  25475  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem2  25552  uniioombllem6  25557  mbfsup  25633  mbfinf  25634  mbflimsup  25635  itg2monolem1  25719  itg2mono  25722  ulm0  26368  pilem2  26430  pilem3  26431  ftalem3  27053  ftalem4  27054  ftalem5  27055  dchrabs  27239  pntlem3  27588  nocvxminlem  27762  bdayfinbndlem1  28475  tglnne0  28724  axlowdim1  29044  nvo00  30848  nmorepnf  30855  minvecolem1  30961  wrdpmtrlast  33186  cycpmco2lem5  33223  elrgspnlem1  33335  primefldchr  33394  fldgensdrg  33407  nsgqusf1olem1  33505  intlidl  33512  idlinsubrg  33523  rhmimaidl  33524  ssdifidl  33549  ssdifidlprm  33550  ssmxidl  33566  pidufd  33635  1arithufdlem1  33636  ply1dg1rtn0  33673  ply1degltlss  33688  exsslsb  33773  constrsdrg  33952  ordtconnlem1  34101  rrhre  34198  sigagenval  34317  oddpwdc  34531  bnj1177  35181  bnj1523  35246  rankfilimbi  35276  erdszelem8  35411  txsconnlem  35453  cvxsconn  35456  cvmsss2  35487  cvmliftmolem2  35495  cvmlift2lem12  35527  cvmliftpht  35531  finminlem  36531  onint1  36662  weiunlem  36676  weiunfr  36680  finxpreclem4  37646  heicant  37903  itg2addnc  37922  ftc1anclem7  37947  ftc1anc  37949  prdsbnd2  38043  lkrlss  39468  pclvalN  40263  dian0  41412  docaclN  41497  dicn0  41565  dihglblem5  41671  dihglb2  41715  doch2val2  41737  dochocss  41739  lclkr  41906  lclkrs  41912  lcfr  41958  aks6d1c6lem3  42539  unitscyglem2  42563  qsalrel  42608  nacsfix  43066  mzpcln0  43082  rencldnfilem  43174  fnwe2lem2  43405  kelac1  43417  harn0  43456  hbtlem2  43478  naddwordnexlem4  43755  omltoe  43760  gneispa  44483  imo72b2lem0  44518  scottrankd  44601  relpfrlem  45306  ubelsupr  45377  suprnmpt  45530  disjinfi  45548  suprubrnmpt2  45607  suprubrnmpt  45608  ssfiunibd  45668  allbutfi  45748  allbutfiinf  45775  uzn0d  45780  uzublem  45785  climinf  45963  limclr  46010  climinf2lem  46061  limsupubuzlem  46067  liminflelimsupuz  46140  cnrefiisplem  46184  ioodvbdlimc1lem1  46286  ioodvbdlimc1  46288  ioodvbdlimc2  46290  stoweidlem36  46391  fourierdlem20  46482  fourierdlem25  46487  fourierdlem31  46493  fourierdlem37  46499  fourierdlem46  46507  fourierdlem52  46513  fourierdlem54  46515  fouriercn  46587  elaa2lem  46588  salgenval  46676  salgenn0  46686  sge0isum  46782  sge0reuzb  46803  ovnlerp  46917  ovnf  46918  hsphoidmvle2  46940  hsphoidmvle  46941  hoiprodp1  46943  hoidmv1lelem1  46946  hoidmv1lelem3  46948  hoidmv1le  46949  hoidifhspdmvle  46975  hspmbllem1  46981  hspmbllem3  46983  ovnovollem2  47012  smflimlem1  47126  smfsuplem1  47166  smfsuplem3  47168  smflimsuplem5  47179  smflimsuplem7  47181  preimafvn0  47737  lincolss  48791  fvconstr2  49220  catprs  49367  discsubc  49420  iinfconstbas  49422  eloppf  49489  eloppf2  49490  oppcup3  49565  oppcthinendcALT  49797  termcterm3  49871  termcciso  49872  idfudiag1bas  49880  idfudiag1  49881