Theorem ne0d 4291

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2957  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3905  df-nul 4283

This theorem is used by:  snnzg  4738  prnzg  4742  eqsnd  4794  exss  5442  isofrlem  7345  peano3  7891  fvmpocurryd  8273  onnseq  8337  oeoalem  8588  oeoelem  8590  oeeui  8594  nnawordex  8629  omxpenlem  9080  frfi  9259  supgtoreq  9445  infltoreq  9478  cantnfp1lem2  9662  cantnfp1lem3  9663  oemapvali  9667  cantnflem1a  9668  cantnflem1d  9671  cantnflem1  9672  epfrs  9714  scottrankd  9892  dfac9  10143  axdc3lem4  10459  intwun  10748  r1limwun  10749  gruina  10831  grur1a  10832  mulclpi  10906  indpi  10920  supsrlem  11124  axpre-sup  11182  supfirege  12230  uzn0  12908  suprzub  12992  fzn0  13596  flval3  13880  icopnfsup  13930  hashelne0d  14436  dfrtrcl2  15139  01sqrexlem3  15335  isercolllem2  15757  isercolllem3  15758  climsup  15761  mertenslem2  15978  gcdcllem1  16595  pclem  16936  prmreclem1  17014  4sqlem13  17055  vdwmc2  17077  vdwlem6  17084  vdwnnlem3  17095  prmgaplem3  17151  prmgaplem4  17152  mrcflem  17700  mrcval  17704  iscatd2  17775  chnub  18716  mndbn0  18859  grpbn0  19096  issubgrpd2  19272  issubg4  19275  subgint  19280  nmzsubg  19294  cycsubgcl  19340  ghmpreima  19371  gastacl  19442  sylow1lem5  19735  pgpssslw  19747  sylow2alem2  19751  sylow2blem3  19755  fislw  19758  sylow3lem4  19763  torsubg  19987  oddvdssubg  19988  iscygd  20020  iscygodd  20021  dprdsubg  20159  ablfac1eu  20208  simpgnideld  20234  submomnd  20265  01eq0ring  20697  cntzsubrng  20735  cntzsubr  20774  imadrhmcl  20969  primefld  20977  primefld0cl  20978  primefld1cl  20979  abvn0b  21008  suborng  21048  islss4  21152  lss1d  21153  lssintcl  21154  lspsolvlem  21335  lbsextlem1  21351  dflidl2rng  21412  lidlsubg  21417  lidlunin0  21430  rhmpreimaidl  21485  ssdifidl  21554  ssdifidlprm  21555  zringlpirlem1  21681  ocvlss  21891  lmiclbs  22056  lmisfree  22061  psrbas  22155  mplsubglem  22219  mplind  22292  mhpsubg  22387  mat1ric  22715  dmatsgrp  22727  scmatsgrp  22747  scmatsgrp1  22750  scmatlss  22753  scmatric  22765  cpmatsubgpmat  22951  matcpmric  22990  pmmpric  23054  clscld  23278  2ndcdisj  23688  dfac14lem  23849  opnfbas  24074  isfil2  24088  filn0  24094  filssufilg  24143  rnelfmlem  24184  flimfnfcls  24260  ptcmplem2  24285  clssubg  24341  tgpconncomp  24345  tsmsfbas  24360  ustfilxp  24445  ustne0  24446  xbln0  24646  bln0  24647  metustfbas  24789  metustbl  24798  nrgdomn  24903  icccmplem2  25056  icccmplem3  25057  reconnlem2  25060  phtpcer  25229  reparpht  25232  phtpcco2  25233  pcohtpy  25254  pcorevlem  25260  isclmp  25331  iscmet3lem2  25526  bcthlem4  25561  minveclem3b  25662  ivthlem2  25686  ivthlem3  25687  evthicc  25693  ovollb2  25723  ovolunlem1a  25730  ovolunlem1  25731  ovoliunlem1  25736  ovoliun2  25740  ioombl1lem4  25795  uniioombllem1  25815  uniioombllem2  25817  uniioombllem6  25822  mbfsup  25898  mbfinf  25899  mbflimsup  25900  itg2monolem1  25984  itg2mono  25987  ulm0  26634  pilem2  26695  pilem3  26696  ftalem3  27319  ftalem4  27320  ftalem5  27321  dchrabs  27504  pntlem3  27853  nocvxminlem  28027  bdayfinbndlem1  28740  tglnne0  28996  tglnpt4  29010  lnoppinn0  29118  angmgmaddeu2  29267  angmgmaddeu3  29268  angmgmaddov2lem  29274  angmgmaddcpbl  29277  angmgmaddrid  29280  prlngmolem1  29317  prlngmolem2  29318  prlngmo2  29321  prlngpln4  29323  prlngsymquadlem  29328  quadcgrprlng  29331  axlowdim1  29424  nvo00  31250  nmorepnf  31257  minvecolem1  31363  wrdpmtrlast  33541  cycpmco2lem5  33578  elrgspnlem1  33690  primefldchr  33750  fldgensdrg  33763  nsgqusf1olem1  33850  intlidl  33856  idlinsubrg  33867  rhmimaidl  33868  ssmxidl  33885  dflringlem2  33913  pidufd  33961  1arithufdlem1  33962  ply1dg1rtn0  33999  ply1degltlss  34014  exsslsb  34115  constrsdrg  34293  ordtconnlem1  34442  rrhre  34539  sigagenval  34659  oddpwdc  34873  bnj1177  35523  bnj1523  35588  rankfilimbi  35617  erdszelem8  35785  txsconnlem  35827  cvxsconn  35830  cvmsss2  35861  cvmliftmolem2  35869  cvmlift2lem12  35901  cvmliftpht  35905  finminlem  36945  onint1  37076  weiunlem  37090  weiunfr  37094  finxpreclem4  38156  heicant  38412  itg2addnc  38431  ftc1anclem7  38456  ftc1anc  38458  prdsbnd2  38553  lkrlss  39976  pclvalN  40771  dian0  41920  docaclN  42005  dicn0  42073  dihglblem5  42179  dihglb2  42223  doch2val2  42245  dochocss  42247  lclkr  42414  lclkrs  42420  lcfr  42466  aks6d1c6lem3  43046  unitscyglem2  43070  qsalrel  43116  nacsfix  43565  mzpcln0  43581  rencldnfilem  43669  fnwe2lem2  43900  kelac1  43912  harn0  43951  hbtlem2  43973  naddwordnexlem4  44250  omltoe  44255  gneispa  44978  imo72b2lem0  45013  relpfrlem  45784  ubelsupr  45862  suprnmpt  46014  disjinfi  46032  suprubrnmpt2  46089  suprubrnmpt  46090  ssfiunibd  46150  allbutfi  46230  allbutfiinf  46256  uzn0d  46261  uzublem  46266  climinf  46444  limclr  46491  climinf2lem  46542  limsupubuzlem  46548  liminflelimsupuz  46621  cnrefiisplem  46665  ioodvbdlimc1lem1  46767  ioodvbdlimc1  46769  ioodvbdlimc2  46771  stoweidlem36  46872  fourierdlem20  46963  fourierdlem25  46968  fourierdlem31  46974  fourierdlem37  46980  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem52  46994  fourierdlem54  46996  fouriercn  47068  elaa2lem  47069  salgenval  47157  salgenn0  47167  sge0isum  47263  sge0reuzb  47284  ovnlerp  47398  ovnf  47399  hsphoidmvle2  47421  hsphoidmvle  47422  hoiprodp1  47424  hoidmv1lelem1  47427  hoidmv1lelem3  47429  hoidmv1le  47430  hoidifhspdmvle  47456  hspmbllem1  47462  hspmbllem3  47464  ovnovollem2  47493  smflimlem1  47607  smfsuplem1  47647  smfsuplem3  47649  smflimsuplem5  47660  smflimsuplem7  47662  preimafvn0  48288  lincolss  49372  fvconstr2  49800  catprs  49945  discsubc  49998  iinfconstbas  50000  eloppf  50067  eloppf2  50068  oppcup3  50143  oppcthinendcALT  50375  termcterm3  50449  termcciso  50450  idfudiag1bas  50458  idfudiag1  50459