Theorem ne0d 4307

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2926  ∅c0 4298

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-dif 3919  df-nul 4299

This theorem is referenced by:  snnzg  4740  prnzg  4744  eqsnd  4796  exss  5425  isofrlem  7317  fvmpocurryd  8252  onnseq  8315  oeoalem  8562  oeoelem  8564  oeeui  8568  nnawordex  8603  omxpenlem  9046  frfi  9238  supgtoreq  9428  infltoreq  9461  cantnfp1lem2  9638  cantnfp1lem3  9639  oemapvali  9643  cantnflem1a  9644  cantnflem1d  9647  cantnflem1  9648  epfrs  9690  dfac9  10096  axdc3lem4  10412  intwun  10694  r1limwun  10695  gruina  10777  grur1a  10778  mulclpi  10852  indpi  10866  supsrlem  11070  axpre-sup  11128  supfirege  12176  uzn0  12816  suprzub  12904  fzn0  13505  flval3  13783  icopnfsup  13833  hashelne0d  14339  dfrtrcl2  15034  01sqrexlem3  15216  isercolllem2  15638  isercolllem3  15639  climsup  15642  mertenslem2  15857  gcdcllem1  16475  pclem  16815  prmreclem1  16893  4sqlem13  16934  vdwmc2  16956  vdwlem6  16963  vdwnnlem3  16974  prmgaplem3  17030  prmgaplem4  17031  mrcflem  17573  mrcval  17577  iscatd2  17648  mndbn0  18683  grpbn0  18904  issubgrpd2  19080  issubg4  19083  subgint  19088  nmzsubg  19103  cycsubgcl  19144  ghmpreima  19176  gastacl  19247  sylow1lem5  19538  pgpssslw  19550  sylow2alem2  19554  sylow2blem3  19558  fislw  19561  sylow3lem4  19566  torsubg  19790  oddvdssubg  19791  iscygd  19823  iscygodd  19824  dprdsubg  19962  ablfac1eu  20011  simpgnideld  20037  01eq0ring  20445  cntzsubrng  20482  cntzsubr  20521  imadrhmcl  20712  primefld  20720  primefld0cl  20721  primefld1cl  20722  abvn0b  20751  islss4  20874  lss1d  20875  lssintcl  20876  lspsolvlem  21058  lbsextlem1  21074  dflidl2rng  21134  lidlsubg  21139  rhmpreimaidl  21193  zringlpirlem1  21378  ocvlss  21587  lmiclbs  21752  lmisfree  21757  psrbas  21848  mplsubglem  21914  mplind  21983  mhpsubg  22046  mat1ric  22380  dmatsgrp  22392  scmatsgrp  22412  scmatsgrp1  22415  scmatlss  22418  scmatric  22430  cpmatsubgpmat  22613  matcpmric  22652  pmmpric  22716  clscld  22940  2ndcdisj  23349  dfac14lem  23510  opnfbas  23735  isfil2  23749  filn0  23755  filssufilg  23804  rnelfmlem  23845  flimfnfcls  23921  ptcmplem2  23946  clssubg  24002  tgpconncomp  24006  tsmsfbas  24021  ustfilxp  24106  ustne0  24107  xbln0  24308  bln0  24309  metustfbas  24451  metustbl  24460  nrgdomn  24565  icccmplem2  24718  icccmplem3  24719  reconnlem2  24722  phtpcer  24900  reparpht  24904  phtpcco2  24905  pcohtpy  24926  pcorevlem  24932  isclmp  25003  iscmet3lem2  25198  bcthlem4  25233  minveclem3b  25334  ivthlem2  25359  ivthlem3  25360  evthicc  25366  ovollb2  25396  ovolunlem1a  25403  ovolunlem1  25404  ovoliunlem1  25409  ovoliun2  25413  ioombl1lem4  25468  uniioombllem1  25488  uniioombllem2  25490  uniioombllem6  25495  mbfsup  25571  mbfinf  25572  mbflimsup  25573  itg2monolem1  25657  itg2mono  25660  ulm0  26306  pilem2  26368  pilem3  26369  ftalem3  26991  ftalem4  26992  ftalem5  26993  dchrabs  27177  pntlem3  27526  nocvxminlem  27695  tglnne0  28573  axlowdim1  28892  nvo00  30696  nmorepnf  30703  minvecolem1  30809  chnub  32944  submomnd  33030  wrdpmtrlast  33056  cycpmco2lem5  33093  elrgspnlem1  33199  primefldchr  33257  fldgensdrg  33270  suborng  33299  nsgqusf1olem1  33390  intlidl  33397  idlinsubrg  33408  rhmimaidl  33409  ssdifidl  33434  ssdifidlprm  33435  ssmxidl  33451  pidufd  33520  1arithufdlem1  33521  ply1dg1rtn0  33555  ply1degltlss  33568  exsslsb  33598  constrsdrg  33771  ordtconnlem1  33920  rrhre  34017  sigagenval  34136  oddpwdc  34351  bnj1177  35002  bnj1523  35067  erdszelem8  35185  txsconnlem  35227  cvxsconn  35230  cvmsss2  35261  cvmliftmolem2  35269  cvmlift2lem12  35301  cvmliftpht  35305  finminlem  36301  onint1  36432  weiunlem2  36446  weiunfr  36450  finxpreclem4  37377  heicant  37644  itg2addnc  37663  ftc1anclem7  37688  ftc1anc  37690  prdsbnd2  37784  lkrlss  39083  pclvalN  39879  dian0  41028  docaclN  41113  dicn0  41181  dihglblem5  41287  dihglb2  41331  doch2val2  41353  dochocss  41355  lclkr  41522  lclkrs  41528  lcfr  41574  aks6d1c6lem3  42155  unitscyglem2  42179  qsalrel  42223  nacsfix  42693  mzpcln0  42709  rencldnfilem  42801  fnwe2lem2  43033  kelac1  43045  harn0  43084  hbtlem2  43106  naddwordnexlem4  43383  omltoe  43389  gneispa  44112  imo72b2lem0  44147  scottrankd  44230  relpfrlem  44936  ubelsupr  45007  suprnmpt  45161  disjinfi  45179  suprubrnmpt2  45239  suprubrnmpt  45240  ssfiunibd  45300  allbutfi  45382  allbutfiinf  45409  uzn0d  45414  uzublem  45419  climinf  45597  limclr  45646  climinf2lem  45697  limsupubuzlem  45703  liminflelimsupuz  45776  cnrefiisplem  45820  ioodvbdlimc1lem1  45922  ioodvbdlimc1  45924  ioodvbdlimc2  45926  stoweidlem36  46027  fourierdlem20  46118  fourierdlem25  46123  fourierdlem31  46129  fourierdlem37  46135  fourierdlem46  46143  fourierdlem52  46149  fourierdlem54  46151  fouriercn  46223  elaa2lem  46224  salgenval  46312  salgenn0  46322  sge0isum  46418  sge0reuzb  46439  ovnlerp  46553  ovnf  46554  hsphoidmvle2  46576  hsphoidmvle  46577  hoiprodp1  46579  hoidmv1lelem1  46582  hoidmv1lelem3  46584  hoidmv1le  46585  hoidifhspdmvle  46611  hspmbllem1  46617  hspmbllem3  46619  ovnovollem2  46648  smflimlem1  46762  smfsuplem1  46802  smfsuplem3  46804  smflimsuplem5  46815  smflimsuplem7  46817  preimafvn0  47371  lincolss  48413  fvconstr2  48840  catprs  48988  discsubc  49041  iinfconstbas  49043  eloppf  49110  eloppf2  49111  oppcup3  49182  oppcthinendcALT  49410  termcterm3  49484  termcciso  49485  idfudiag1bas  49493  idfudiag1  49494