Theorem ssidd 3938

Description: Weakening of ssid 3937. (Contributed by BJ, 1-Sep-2022.)

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

Step	Hyp	Ref	Expression
1		ssid 3937	. 2 ⊢ 𝐴 ⊆ 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  funfvima2d  6972  suppofss1d  7851  suppofss2d  7852  ralxpmap  8443  fissuni  8813  fsuppmptif  8847  fsuppco2  8850  fsuppcor  8851  mapfienlem1  8852  mapfienlem2  8853  cantnfp1lem1  9125  cantnfp1lem3  9127  cantnflem1  9136  htalem  9309  ackbij2lem4  9653  cflim2  9674  fin23lem15  9745  wunex2  10149  swrd0  14011  rtrclreclem1  14408  summolem3  15063  isum  15068  fsumser  15079  fsumcl  15082  flo1  15201  prodmolem3  15279  iprod  15284  iprodn0  15286  fprodss  15294  fprodcl  15298  fprodclf  15338  rpnnen2lem11  15569  eulerthlem2  16109  mremre  16867  catsubcat  17101  yon11  17506  yon12  17507  yon2  17508  yonpropd  17510  oppcyon  17511  yonffth  17526  submid  17967  mulgnncl  18235  mulgnn0cl  18236  mulgcl  18237  subgid  18273  snsymgefmndeq  18515  symggen  18590  gsumzcl2  19023  gsumzf1o  19025  gsum2dlem1  19083  gsum2dlem2  19084  gsum2d  19085  gsumxp2  19093  dprdfinv  19134  dmdprdsplitlem  19152  dprd2db  19158  dpjidcl  19173  ablfac1eu  19188  ablfaclem2  19201  gsumdixp  19355  primefld  19577  lcomfsupp  19667  lss1  19703  rlmbas  19960  rlmplusg  19961  rlm0  19962  rlmmulr  19964  rlmsca  19965  rlmsca2  19966  rlmvsca  19967  rlmtopn  19968  rlmds  19969  regsumsupp  20311  frlmsslsp  20485  frlmup1  20487  rnasclassa  20581  mplsubglem  20672  mpllsslem  20673  mplsubrglem  20677  mplcoe1  20705  mplcoe5  20708  mplbas2  20710  evlslem4  20747  psrbagev1  20749  evlslem2  20751  mhpvscacl  20802  mamures  20997  cpmadumatpolylem2  21487  neiptopuni  21735  neiptoptop  21736  restopn2  21782  rncmp  22001  cmpfi  22013  conncn  22031  llyidm  22093  nllyidm  22094  toplly  22095  kgentopon  22143  kgencn2  22162  ptcld  22218  qtopuni  22307  supnfcls  22625  utopbas  22841  metustfbas  23164  rrxcph  23996  rrxmval  24009  rrxdstprj1  24013  evthicc2  24064  volcn  24210  dvres3  24516  dvres3a  24517  dvidlem  24518  dvmptresicc  24519  dvnadd  24532  dvnres  24534  dvaddbr  24541  dvmulbr  24542  dvcmul  24547  dvcmulf  24548  dvcobr  24549  dvcjbr  24552  dvrec  24558  dveflem  24582  dvef  24583  dvlipcn  24597  dvgt0lem2  24606  lhop1lem  24616  ftc1cn  24646  ftc2  24647  itgpowd  24653  deg1mul3le  24717  coeeulem  24821  dgrcolem1  24870  dgrcolem2  24871  plycpn  24885  dvntaylp  24966  pserdv  25024  pige3ALT  25112  cxpcn2  25335  rlimcnp3  25553  lgamgulmlem2  25615  basellem2  25667  pntrsumo1  26149  pntrsumbnd  26150  nbupgr  27134  nbumgrvtx  27136  nbgr2vtx1edg  27140  cusgrexilem2  27232  ifpsnprss  27412  1pthon2ve  27939  suppovss  30443  offinsupp1  30489  xrsmulgzz  30712  gsummpt2co  30733  gsumpart  30740  gsumhashmul  30741  symgcom2  30778  pmtrcnelor  30785  tocycfvres1  30802  tocycfvres2  30803  cycpmconjvlem  30833  lindfpropd  30996  lsmsnpridl  31005  elrspunidl  31014  mxidlprm  31048  ssmxidl  31050  rgmoddim  31096  tngdim  31099  matdim  31101  fedgmullem1  31113  mdetpmtr1  31176  zarclssn  31226  zart0  31232  zarcmplem  31234  pnfneige0  31304  pwsiga  31499  baselcarsg  31674  efmul2picn  31977  reprfz1  32005  breprexplemc  32013  circlemeth  32021  circlevma  32023  circlemethhgt  32024  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  satfsschain  32724  mrsubff1  32874  mrsub0  32876  mrsubccat  32878  mrsubcn  32879  msubff1  32916  mthmpps  32942  trpredpo  33187  wzel  33224  fpr1  33252  nosupbnd1lem1  33321  knoppndvlem6  33969  knoppndv  33986  bj-elpwg  34469  bj-restpw  34507  bj-restb  34509  bj-restuni2  34513  ftc1cnnclem  35128  ftc1cnnc  35129  ftc2nc  35139  areacirclem3  35147  welb  35174  cnresima  35202  rngoidl  35462  1psubclN  37240  cdlemefrs32fva  37696  lcmineqlem9  39325  lcmineqlem12  39328  intlewftc  39344  selvval2lem4  39431  addinvcom  39568  rgspnid  40116  harval3  40244  cnvtrucl0  40324  brfvrtrcld  40435  clsk3nimkb  40743  k0004ss2  40855  extoimad  40868  mnuprd  40984  dvconstbi  41038  ssinc  41723  ssdec  41724  founiiun  41803  choicefi  41829  islptre  42261  fnlimfvre  42316  addccncf2  42518  fsumcncf  42520  cncfperiod  42521  negcncfg  42523  cncfuni  42528  icccncfext  42529  cncficcgt0  42530  fprodcncf  42542  dvcnre  42558  fperdvper  42561  itgsinexplem1  42596  itgcoscmulx  42611  submgmid  44413  rnghmsscmap2  44597  rhmsscmap2  44643  fldhmsubc  44708  fldhmsubcALTV  44726  elbigolo1  44971