Theorem ne0d 4270

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2944  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-dif 3891  df-nul 4258

This theorem is referenced by:  snnzg  4711  prnzg  4715  exss  5379  isofrlem  7220  fvmpocurryd  8096  onnseq  8184  oeoalem  8436  oeoelem  8438  oeeui  8442  nnawordex  8477  omxpenlem  8869  frfi  9068  supgtoreq  9238  infltoreq  9270  cantnfp1lem2  9446  cantnfp1lem3  9447  oemapvali  9451  cantnflem1a  9452  cantnflem1d  9455  cantnflem1  9456  epfrs  9498  dfac9  9901  axdc3lem4  10218  intwun  10500  r1limwun  10501  gruina  10583  grur1a  10584  mulclpi  10658  indpi  10672  supsrlem  10876  axpre-sup  10934  supfirege  11971  uzn0  12608  suprzub  12688  fzn0  13279  flval3  13544  icopnfsup  13594  hashelne0d  14092  dfrtrcl2  14782  sqrlem3  14965  isercolllem2  15386  isercolllem3  15387  climsup  15390  mertenslem2  15606  gcdcllem1  16215  pclem  16548  prmreclem1  16626  4sqlem13  16667  vdwmc2  16689  vdwlem6  16696  vdwnnlem3  16707  prmgaplem3  16763  prmgaplem4  16764  mrcflem  17324  mrcval  17328  iscatd2  17399  mndbn0  18410  grpbn0  18617  issubgrpd2  18780  issubg4  18783  subgint  18788  nmzsubg  18802  cycsubgcl  18834  ghmpreima  18865  gastacl  18924  sylow1lem5  19216  pgpssslw  19228  sylow2alem2  19232  sylow2blem3  19236  fislw  19239  sylow3lem4  19244  torsubg  19464  oddvdssubg  19465  iscygd  19496  iscygodd  19497  dprdsubg  19636  ablfac1eu  19685  simpgnideld  19711  cntzsubr  20066  primefld  20082  primefld0cl  20083  primefld1cl  20084  islss4  20233  lss1d  20234  lssintcl  20235  lspsolvlem  20413  lbsextlem1  20429  lidlsubg  20495  abvn0b  20582  zringlpirlem1  20693  ocvlss  20886  lmiclbs  21053  lmisfree  21058  psrbas  21156  mplsubglem  21214  mplind  21287  mhpsubg  21352  mat1ric  21645  dmatsgrp  21657  scmatsgrp  21677  scmatsgrp1  21680  scmatlss  21683  scmatric  21695  cpmatsubgpmat  21878  matcpmric  21917  pmmpric  21981  clscld  22207  2ndcdisj  22616  dfac14lem  22777  opnfbas  23002  isfil2  23016  filn0  23022  filssufilg  23071  rnelfmlem  23112  flimfnfcls  23188  ptcmplem2  23213  clssubg  23269  tgpconncomp  23273  tsmsfbas  23288  ustfilxp  23373  ustne0  23374  xbln0  23576  bln0  23577  metustfbas  23722  metustbl  23731  nrgdomn  23844  icccmplem2  23995  icccmplem3  23996  reconnlem2  23999  phtpcer  24167  reparpht  24170  phtpcco2  24171  pcohtpy  24192  pcorevlem  24198  isclmp  24269  iscmet3lem2  24465  bcthlem4  24500  minveclem3b  24601  ivthlem2  24625  ivthlem3  24626  evthicc  24632  ovollb2  24662  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliun2  24679  ioombl1lem4  24734  uniioombllem1  24754  uniioombllem2  24756  uniioombllem6  24761  mbfsup  24837  mbfinf  24838  mbflimsup  24839  itg2monolem1  24924  itg2mono  24927  ulm0  25559  pilem2  25620  pilem3  25621  ftalem3  26233  ftalem4  26234  ftalem5  26235  dchrabs  26417  pntlem3  26766  tglnne0  27010  axlowdim1  27336  nvo00  29132  nmorepnf  29139  minvecolem1  29245  submomnd  31345  cycpmco2lem5  31406  primefldchr  31502  suborng  31523  nsgqusf1olem1  31607  intlidl  31611  rhmpreimaidl  31612  idlinsubrg  31617  rhmimaidl  31618  ssmxidl  31651  ordtconnlem1  31883  rrhre  31980  sigagenval  32117  oddpwdc  32330  bnj1177  32995  bnj1523  33060  erdszelem8  33169  txsconnlem  33211  cvxsconn  33214  cvmsss2  33245  cvmliftmolem2  33253  cvmlift2lem12  33285  cvmliftpht  33289  nocvxminlem  33981  finminlem  34516  onint1  34647  finxpreclem4  35574  heicant  35821  itg2addnc  35840  ftc1anclem7  35865  ftc1anc  35867  prdsbnd2  35962  lkrlss  37116  pclvalN  37911  dian0  39060  docaclN  39145  dicn0  39213  dihglblem5  39319  dihglb2  39363  doch2val2  39385  dochocss  39387  lclkr  39554  lclkrs  39560  lcfr  39606  qsalrel  40222  prjcrv0  40477  nacsfix  40541  mzpcln0  40557  rencldnfilem  40649  fnwe2lem2  40883  kelac1  40895  harn0  40934  hbtlem2  40956  gneispa  41747  scottrankd  41873  ubelsupr  42570  suprnmpt  42717  disjinfi  42738  suprubrnmpt2  42805  suprubrnmpt  42806  ssfiunibd  42855  allbutfi  42940  allbutfiinf  42967  uzn0d  42972  uzublem  42977  climinf  43154  limclr  43203  climinf2lem  43254  limsupubuzlem  43260  liminflelimsupuz  43333  cnrefiisplem  43377  ioodvbdlimc1lem1  43479  ioodvbdlimc1  43481  ioodvbdlimc2  43483  stoweidlem36  43584  fourierdlem20  43675  fourierdlem25  43680  fourierdlem31  43686  fourierdlem37  43692  fourierdlem46  43700  fourierdlem52  43706  fourierdlem54  43708  fouriercn  43780  elaa2lem  43781  salgenval  43869  salgenn0  43877  sge0isum  43972  sge0reuzb  43993  ovnlerp  44107  ovnf  44108  hsphoidmvle2  44130  hsphoidmvle  44131  hoiprodp1  44133  hoidmv1lelem1  44136  hoidmv1lelem3  44138  hoidmv1le  44139  hoidifhspdmvle  44165  hspmbllem1  44171  hspmbllem3  44173  ovnovollem2  44202  smflimlem1  44316  smfsuplem1  44355  smfsuplem3  44357  smflimsuplem5  44368  smflimsuplem7  44370  preimafvn0  44843  lincolss  45786  fvconstr2  46196  catprs  46303