Theorem ne0d 4347

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2937  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-dif 3965  df-nul 4339

This theorem is referenced by:  snnzg  4778  prnzg  4782  eqsnd  4834  exss  5473  isofrlem  7359  fvmpocurryd  8294  onnseq  8382  oeoalem  8632  oeoelem  8634  oeeui  8638  nnawordex  8673  omxpenlem  9111  frfi  9318  supgtoreq  9507  infltoreq  9539  cantnfp1lem2  9716  cantnfp1lem3  9717  oemapvali  9721  cantnflem1a  9722  cantnflem1d  9725  cantnflem1  9726  epfrs  9768  dfac9  10174  axdc3lem4  10490  intwun  10772  r1limwun  10773  gruina  10855  grur1a  10856  mulclpi  10930  indpi  10944  supsrlem  11148  axpre-sup  11206  supfirege  12252  uzn0  12892  suprzub  12978  fzn0  13574  flval3  13851  icopnfsup  13901  hashelne0d  14403  dfrtrcl2  15097  01sqrexlem3  15279  isercolllem2  15698  isercolllem3  15699  climsup  15702  mertenslem2  15917  gcdcllem1  16532  pclem  16871  prmreclem1  16949  4sqlem13  16990  vdwmc2  17012  vdwlem6  17019  vdwnnlem3  17030  prmgaplem3  17086  prmgaplem4  17087  mrcflem  17650  mrcval  17654  iscatd2  17725  mndbn0  18775  grpbn0  18996  issubgrpd2  19172  issubg4  19175  subgint  19180  nmzsubg  19195  cycsubgcl  19236  ghmpreima  19268  gastacl  19339  sylow1lem5  19634  pgpssslw  19646  sylow2alem2  19650  sylow2blem3  19654  fislw  19657  sylow3lem4  19662  torsubg  19886  oddvdssubg  19887  iscygd  19919  iscygodd  19920  dprdsubg  20058  ablfac1eu  20107  simpgnideld  20133  01eq0ring  20546  cntzsubrng  20583  cntzsubr  20622  imadrhmcl  20814  primefld  20822  primefld0cl  20823  primefld1cl  20824  abvn0b  20853  islss4  20977  lss1d  20978  lssintcl  20979  lspsolvlem  21161  lbsextlem1  21177  dflidl2rng  21245  lidlsubg  21250  rhmpreimaidl  21304  zringlpirlem1  21490  ocvlss  21707  lmiclbs  21874  lmisfree  21879  psrbas  21970  mplsubglem  22036  mplind  22111  mhpsubg  22174  mat1ric  22508  dmatsgrp  22520  scmatsgrp  22540  scmatsgrp1  22543  scmatlss  22546  scmatric  22558  cpmatsubgpmat  22741  matcpmric  22780  pmmpric  22844  clscld  23070  2ndcdisj  23479  dfac14lem  23640  opnfbas  23865  isfil2  23879  filn0  23885  filssufilg  23934  rnelfmlem  23975  flimfnfcls  24051  ptcmplem2  24076  clssubg  24132  tgpconncomp  24136  tsmsfbas  24151  ustfilxp  24236  ustne0  24237  xbln0  24439  bln0  24440  metustfbas  24585  metustbl  24594  nrgdomn  24707  icccmplem2  24858  icccmplem3  24859  reconnlem2  24862  phtpcer  25040  reparpht  25044  phtpcco2  25045  pcohtpy  25066  pcorevlem  25072  isclmp  25143  iscmet3lem2  25339  bcthlem4  25374  minveclem3b  25475  ivthlem2  25500  ivthlem3  25501  evthicc  25507  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun2  25554  ioombl1lem4  25609  uniioombllem1  25629  uniioombllem2  25631  uniioombllem6  25636  mbfsup  25712  mbfinf  25713  mbflimsup  25714  itg2monolem1  25799  itg2mono  25802  ulm0  26448  pilem2  26510  pilem3  26511  ftalem3  27132  ftalem4  27133  ftalem5  27134  dchrabs  27318  pntlem3  27667  nocvxminlem  27836  tglnne0  28662  axlowdim1  28988  nvo00  30789  nmorepnf  30796  minvecolem1  30902  chnub  32985  submomnd  33069  wrdpmtrlast  33095  cycpmco2lem5  33132  elrgspnlem1  33231  primefldchr  33282  fldgensdrg  33295  suborng  33324  nsgqusf1olem1  33420  intlidl  33427  idlinsubrg  33438  rhmimaidl  33439  ssdifidl  33464  ssdifidlprm  33465  ssmxidl  33481  pidufd  33550  1arithufdlem1  33551  ply1dg1rtn0  33584  ply1degltlss  33596  ordtconnlem1  33884  rrhre  33983  sigagenval  34120  oddpwdc  34335  bnj1177  34998  bnj1523  35063  erdszelem8  35182  txsconnlem  35224  cvxsconn  35227  cvmsss2  35258  cvmliftmolem2  35266  cvmlift2lem12  35298  cvmliftpht  35302  finminlem  36300  onint1  36431  weiunlem2  36445  weiunfr  36449  finxpreclem4  37376  heicant  37641  itg2addnc  37660  ftc1anclem7  37685  ftc1anc  37687  prdsbnd2  37781  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  42153  unitscyglem2  42177  qsalrel  42259  nacsfix  42699  mzpcln0  42715  rencldnfilem  42807  fnwe2lem2  43039  kelac1  43051  harn0  43090  hbtlem2  43112  naddwordnexlem4  43390  omltoe  43396  gneispa  44119  imo72b2lem0  44154  scottrankd  44243  ubelsupr  44957  suprnmpt  45116  disjinfi  45134  suprubrnmpt2  45196  suprubrnmpt  45197  ssfiunibd  45259  allbutfi  45342  allbutfiinf  45369  uzn0d  45374  uzublem  45379  climinf  45561  limclr  45610  climinf2lem  45661  limsupubuzlem  45667  liminflelimsupuz  45740  cnrefiisplem  45784  ioodvbdlimc1lem1  45886  ioodvbdlimc1  45888  ioodvbdlimc2  45890  stoweidlem36  45991  fourierdlem20  46082  fourierdlem25  46087  fourierdlem31  46093  fourierdlem37  46099  fourierdlem46  46107  fourierdlem52  46113  fourierdlem54  46115  fouriercn  46187  elaa2lem  46188  salgenval  46276  salgenn0  46286  sge0isum  46382  sge0reuzb  46403  ovnlerp  46517  ovnf  46518  hsphoidmvle2  46540  hsphoidmvle  46541  hoiprodp1  46543  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmv1le  46549  hoidifhspdmvle  46575  hspmbllem1  46581  hspmbllem3  46583  ovnovollem2  46612  smflimlem1  46726  smfsuplem1  46766  smfsuplem3  46768  smflimsuplem5  46779  smflimsuplem7  46781  preimafvn0  47304  lincolss  48279  fvconstr2  48687  catprs  48799