Theorem ne0d 4308

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

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

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 3920  df-nul 4300

This theorem is referenced by:  snnzg  4741  prnzg  4745  eqsnd  4797  exss  5426  isofrlem  7318  fvmpocurryd  8253  onnseq  8316  oeoalem  8563  oeoelem  8565  oeeui  8569  nnawordex  8604  omxpenlem  9047  frfi  9239  supgtoreq  9429  infltoreq  9462  cantnfp1lem2  9639  cantnfp1lem3  9640  oemapvali  9644  cantnflem1a  9645  cantnflem1d  9648  cantnflem1  9649  epfrs  9691  dfac9  10097  axdc3lem4  10413  intwun  10695  r1limwun  10696  gruina  10778  grur1a  10779  mulclpi  10853  indpi  10867  supsrlem  11071  axpre-sup  11129  supfirege  12177  uzn0  12817  suprzub  12905  fzn0  13506  flval3  13784  icopnfsup  13834  hashelne0d  14340  dfrtrcl2  15035  01sqrexlem3  15217  isercolllem2  15639  isercolllem3  15640  climsup  15643  mertenslem2  15858  gcdcllem1  16476  pclem  16816  prmreclem1  16894  4sqlem13  16935  vdwmc2  16957  vdwlem6  16964  vdwnnlem3  16975  prmgaplem3  17031  prmgaplem4  17032  mrcflem  17574  mrcval  17578  iscatd2  17649  mndbn0  18684  grpbn0  18905  issubgrpd2  19081  issubg4  19084  subgint  19089  nmzsubg  19104  cycsubgcl  19145  ghmpreima  19177  gastacl  19248  sylow1lem5  19539  pgpssslw  19551  sylow2alem2  19555  sylow2blem3  19559  fislw  19562  sylow3lem4  19567  torsubg  19791  oddvdssubg  19792  iscygd  19824  iscygodd  19825  dprdsubg  19963  ablfac1eu  20012  simpgnideld  20038  01eq0ring  20446  cntzsubrng  20483  cntzsubr  20522  imadrhmcl  20713  primefld  20721  primefld0cl  20722  primefld1cl  20723  abvn0b  20752  islss4  20875  lss1d  20876  lssintcl  20877  lspsolvlem  21059  lbsextlem1  21075  dflidl2rng  21135  lidlsubg  21140  rhmpreimaidl  21194  zringlpirlem1  21379  ocvlss  21588  lmiclbs  21753  lmisfree  21758  psrbas  21849  mplsubglem  21915  mplind  21984  mhpsubg  22047  mat1ric  22381  dmatsgrp  22393  scmatsgrp  22413  scmatsgrp1  22416  scmatlss  22419  scmatric  22431  cpmatsubgpmat  22614  matcpmric  22653  pmmpric  22717  clscld  22941  2ndcdisj  23350  dfac14lem  23511  opnfbas  23736  isfil2  23750  filn0  23756  filssufilg  23805  rnelfmlem  23846  flimfnfcls  23922  ptcmplem2  23947  clssubg  24003  tgpconncomp  24007  tsmsfbas  24022  ustfilxp  24107  ustne0  24108  xbln0  24309  bln0  24310  metustfbas  24452  metustbl  24461  nrgdomn  24566  icccmplem2  24719  icccmplem3  24720  reconnlem2  24723  phtpcer  24901  reparpht  24905  phtpcco2  24906  pcohtpy  24927  pcorevlem  24933  isclmp  25004  iscmet3lem2  25199  bcthlem4  25234  minveclem3b  25335  ivthlem2  25360  ivthlem3  25361  evthicc  25367  ovollb2  25397  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun2  25414  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem2  25491  uniioombllem6  25496  mbfsup  25572  mbfinf  25573  mbflimsup  25574  itg2monolem1  25658  itg2mono  25661  ulm0  26307  pilem2  26369  pilem3  26370  ftalem3  26992  ftalem4  26993  ftalem5  26994  dchrabs  27178  pntlem3  27527  nocvxminlem  27696  tglnne0  28574  axlowdim1  28893  nvo00  30697  nmorepnf  30704  minvecolem1  30810  chnub  32945  submomnd  33031  wrdpmtrlast  33057  cycpmco2lem5  33094  elrgspnlem1  33200  primefldchr  33258  fldgensdrg  33271  suborng  33300  nsgqusf1olem1  33391  intlidl  33398  idlinsubrg  33409  rhmimaidl  33410  ssdifidl  33435  ssdifidlprm  33436  ssmxidl  33452  pidufd  33521  1arithufdlem1  33522  ply1dg1rtn0  33556  ply1degltlss  33569  exsslsb  33599  constrsdrg  33772  ordtconnlem1  33921  rrhre  34018  sigagenval  34137  oddpwdc  34352  bnj1177  35003  bnj1523  35068  erdszelem8  35192  txsconnlem  35234  cvxsconn  35237  cvmsss2  35268  cvmliftmolem2  35276  cvmlift2lem12  35308  cvmliftpht  35312  finminlem  36313  onint1  36444  weiunlem2  36458  weiunfr  36462  finxpreclem4  37389  heicant  37656  itg2addnc  37675  ftc1anclem7  37700  ftc1anc  37702  prdsbnd2  37796  lkrlss  39095  pclvalN  39891  dian0  41040  docaclN  41125  dicn0  41193  dihglblem5  41299  dihglb2  41343  doch2val2  41365  dochocss  41367  lclkr  41534  lclkrs  41540  lcfr  41586  aks6d1c6lem3  42167  unitscyglem2  42191  qsalrel  42235  nacsfix  42707  mzpcln0  42723  rencldnfilem  42815  fnwe2lem2  43047  kelac1  43059  harn0  43098  hbtlem2  43120  naddwordnexlem4  43397  omltoe  43403  gneispa  44126  imo72b2lem0  44161  scottrankd  44244  relpfrlem  44950  ubelsupr  45021  suprnmpt  45175  disjinfi  45193  suprubrnmpt2  45253  suprubrnmpt  45254  ssfiunibd  45314  allbutfi  45396  allbutfiinf  45423  uzn0d  45428  uzublem  45433  climinf  45611  limclr  45660  climinf2lem  45711  limsupubuzlem  45717  liminflelimsupuz  45790  cnrefiisplem  45834  ioodvbdlimc1lem1  45936  ioodvbdlimc1  45938  ioodvbdlimc2  45940  stoweidlem36  46041  fourierdlem20  46132  fourierdlem25  46137  fourierdlem31  46143  fourierdlem37  46149  fourierdlem46  46157  fourierdlem52  46163  fourierdlem54  46165  fouriercn  46237  elaa2lem  46238  salgenval  46326  salgenn0  46336  sge0isum  46432  sge0reuzb  46453  ovnlerp  46567  ovnf  46568  hsphoidmvle2  46590  hsphoidmvle  46591  hoiprodp1  46593  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmv1le  46599  hoidifhspdmvle  46625  hspmbllem1  46631  hspmbllem3  46633  ovnovollem2  46662  smflimlem1  46776  smfsuplem1  46816  smfsuplem3  46818  smflimsuplem5  46829  smflimsuplem7  46831  preimafvn0  47385  lincolss  48427  fvconstr2  48856  catprs  49004  discsubc  49057  iinfconstbas  49059  eloppf  49126  eloppf2  49127  oppcup3  49202  oppcthinendcALT  49434  termcterm3  49508  termcciso  49509  idfudiag1bas  49517  idfudiag1  49518