Theorem ne0d 4365

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-dif 3979  df-nul 4353

This theorem is referenced by:  snnzg  4799  prnzg  4803  eqsnd  4855  exss  5483  isofrlem  7376  fvmpocurryd  8312  onnseq  8400  oeoalem  8652  oeoelem  8654  oeeui  8658  nnawordex  8693  omxpenlem  9139  frfi  9349  supgtoreq  9539  infltoreq  9571  cantnfp1lem2  9748  cantnfp1lem3  9749  oemapvali  9753  cantnflem1a  9754  cantnflem1d  9757  cantnflem1  9758  epfrs  9800  dfac9  10206  axdc3lem4  10522  intwun  10804  r1limwun  10805  gruina  10887  grur1a  10888  mulclpi  10962  indpi  10976  supsrlem  11180  axpre-sup  11238  supfirege  12282  uzn0  12920  suprzub  13004  fzn0  13598  flval3  13866  icopnfsup  13916  hashelne0d  14417  dfrtrcl2  15111  01sqrexlem3  15293  isercolllem2  15714  isercolllem3  15715  climsup  15718  mertenslem2  15933  gcdcllem1  16545  pclem  16885  prmreclem1  16963  4sqlem13  17004  vdwmc2  17026  vdwlem6  17033  vdwnnlem3  17044  prmgaplem3  17100  prmgaplem4  17101  mrcflem  17664  mrcval  17668  iscatd2  17739  mndbn0  18788  grpbn0  19006  issubgrpd2  19182  issubg4  19185  subgint  19190  nmzsubg  19205  cycsubgcl  19246  ghmpreima  19278  gastacl  19349  sylow1lem5  19644  pgpssslw  19656  sylow2alem2  19660  sylow2blem3  19664  fislw  19667  sylow3lem4  19672  torsubg  19896  oddvdssubg  19897  iscygd  19929  iscygodd  19930  dprdsubg  20068  ablfac1eu  20117  simpgnideld  20143  01eq0ring  20556  cntzsubrng  20593  cntzsubr  20634  imadrhmcl  20820  primefld  20828  primefld0cl  20829  primefld1cl  20830  abvn0b  20859  islss4  20983  lss1d  20984  lssintcl  20985  lspsolvlem  21167  lbsextlem1  21183  dflidl2rng  21251  lidlsubg  21256  rhmpreimaidl  21310  zringlpirlem1  21496  ocvlss  21713  lmiclbs  21880  lmisfree  21885  psrbas  21976  mplsubglem  22042  mplind  22117  mhpsubg  22180  mat1ric  22514  dmatsgrp  22526  scmatsgrp  22546  scmatsgrp1  22549  scmatlss  22552  scmatric  22564  cpmatsubgpmat  22747  matcpmric  22786  pmmpric  22850  clscld  23076  2ndcdisj  23485  dfac14lem  23646  opnfbas  23871  isfil2  23885  filn0  23891  filssufilg  23940  rnelfmlem  23981  flimfnfcls  24057  ptcmplem2  24082  clssubg  24138  tgpconncomp  24142  tsmsfbas  24157  ustfilxp  24242  ustne0  24243  xbln0  24445  bln0  24446  metustfbas  24591  metustbl  24600  nrgdomn  24713  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  phtpcer  25046  reparpht  25050  phtpcco2  25051  pcohtpy  25072  pcorevlem  25078  isclmp  25149  iscmet3lem2  25345  bcthlem4  25380  minveclem3b  25481  ivthlem2  25506  ivthlem3  25507  evthicc  25513  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem6  25642  mbfsup  25718  mbfinf  25719  mbflimsup  25720  itg2monolem1  25805  itg2mono  25808  ulm0  26452  pilem2  26514  pilem3  26515  ftalem3  27136  ftalem4  27137  ftalem5  27138  dchrabs  27322  pntlem3  27671  nocvxminlem  27840  tglnne0  28666  axlowdim1  28992  nvo00  30793  nmorepnf  30800  minvecolem1  30906  chnub  32984  submomnd  33060  wrdpmtrlast  33086  cycpmco2lem5  33123  primefldchr  33268  fldgensdrg  33281  suborng  33310  nsgqusf1olem1  33406  intlidl  33413  idlinsubrg  33424  rhmimaidl  33425  ssdifidl  33450  ssdifidlprm  33451  ssmxidl  33467  pidufd  33536  1arithufdlem1  33537  ply1dg1rtn0  33570  ply1degltlss  33582  ordtconnlem1  33870  rrhre  33967  sigagenval  34104  oddpwdc  34319  bnj1177  34982  bnj1523  35047  erdszelem8  35166  txsconnlem  35208  cvxsconn  35211  cvmsss2  35242  cvmliftmolem2  35250  cvmlift2lem12  35282  cvmliftpht  35286  finminlem  36284  onint1  36415  weiunlem2  36429  weiunfr  36433  finxpreclem4  37360  heicant  37615  itg2addnc  37634  ftc1anclem7  37659  ftc1anc  37661  prdsbnd2  37755  lkrlss  39051  pclvalN  39847  dian0  40996  docaclN  41081  dicn0  41149  dihglblem5  41255  dihglb2  41299  doch2val2  41321  dochocss  41323  lclkr  41490  lclkrs  41496  lcfr  41542  aks6d1c6lem3  42129  unitscyglem2  42153  qsalrel  42235  nacsfix  42668  mzpcln0  42684  rencldnfilem  42776  fnwe2lem2  43008  kelac1  43020  harn0  43059  hbtlem2  43081  naddwordnexlem4  43363  omltoe  43369  gneispa  44092  scottrankd  44217  ubelsupr  44920  suprnmpt  45081  disjinfi  45099  suprubrnmpt2  45161  suprubrnmpt  45162  ssfiunibd  45224  allbutfi  45308  allbutfiinf  45335  uzn0d  45340  uzublem  45345  climinf  45527  limclr  45576  climinf2lem  45627  limsupubuzlem  45633  liminflelimsupuz  45706  cnrefiisplem  45750  ioodvbdlimc1lem1  45852  ioodvbdlimc1  45854  ioodvbdlimc2  45856  stoweidlem36  45957  fourierdlem20  46048  fourierdlem25  46053  fourierdlem31  46059  fourierdlem37  46065  fourierdlem46  46073  fourierdlem52  46079  fourierdlem54  46081  fouriercn  46153  elaa2lem  46154  salgenval  46242  salgenn0  46252  sge0isum  46348  sge0reuzb  46369  ovnlerp  46483  ovnf  46484  hsphoidmvle2  46506  hsphoidmvle  46507  hoiprodp1  46509  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmv1le  46515  hoidifhspdmvle  46541  hspmbllem1  46547  hspmbllem3  46549  ovnovollem2  46578  smflimlem1  46692  smfsuplem1  46732  smfsuplem3  46734  smflimsuplem5  46745  smflimsuplem7  46747  preimafvn0  47254  lincolss  48163  fvconstr2  48571  catprs  48678