Theorem ssidd 4005

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  funfvima2d  7236  suppofss1d  8191  suppofss2d  8192  fpr1  8290  ralxpmap  8892  fissuni  9359  fsuppmptif  9396  fsuppco2  9400  fsuppcor  9401  mapfienlem1  9402  mapfienlem2  9403  cantnfp1lem1  9675  cantnfp1lem3  9677  cantnflem1  9686  htalem  9893  ackbij2lem4  10239  cflim2  10260  fin23lem15  10331  wunex2  10735  swrd0  14612  rtrclreclem1  15008  summolem3  15664  isum  15669  fsumser  15680  fsumcl  15683  flo1  15804  prodmolem3  15881  iprod  15886  iprodn0  15888  fprodss  15896  fprodcl  15900  fprodclf  15940  rpnnen2lem11  16171  eulerthlem2  16719  mremre  17552  catsubcat  17793  yon11  18221  yon12  18222  yon2  18223  yonpropd  18225  oppcyon  18226  yonffth  18241  submgmid  18631  submid  18727  mulgnncl  19005  mulgnn0cl  19006  mulgcl  19007  subgid  19044  snsymgefmndeq  19303  symggen  19379  gsumzcl2  19819  gsumzf1o  19821  gsum2dlem1  19879  gsum2dlem2  19880  gsum2d  19881  gsumxp2  19889  dprdfinv  19930  dmdprdsplitlem  19948  dprd2db  19954  dpjidcl  19969  ablfac1eu  19984  ablfaclem2  19997  gsumdixp  20207  subrngid  20437  primefld  20564  lcomfsupp  20656  lss1  20693  rlmbas  20962  rlmplusg  20963  rlm0  20964  rlmmulr  20966  rlmsca  20967  rlmsca2  20968  rlmvsca  20969  rlmtopn  20970  rlmds  20971  rng2idl1cntr  21064  regsumsupp  21394  frlmsslsp  21570  frlmup1  21572  rnasclassa  21668  mplsubglem  21777  mpllsslem  21778  mplsubrglem  21782  mplcoe1  21811  mplcoe5  21814  mplbas2  21816  evlslem4  21856  psrbagev1  21857  psrbagev1OLD  21858  evlslem2  21861  mhpvscacl  21916  mamures  22112  cpmadumatpolylem2  22604  neiptopuni  22854  neiptoptop  22855  restopn2  22901  rncmp  23120  cmpfi  23132  conncn  23150  llyidm  23212  nllyidm  23213  toplly  23214  kgentopon  23262  kgencn2  23281  ptcld  23337  qtopuni  23426  supnfcls  23744  utopbas  23960  metustfbas  24286  rrxcph  25133  rrxmval  25146  rrxdstprj1  25150  evthicc2  25201  volcn  25347  dvres3  25654  dvres3a  25655  dvidlem  25656  dvmptresicc  25657  dvnadd  25670  dvnres  25672  dvaddbr  25679  dvmulbr  25680  dvcmul  25685  dvcmulf  25686  dvcobr  25687  dvcjbr  25690  dvrec  25696  dveflem  25720  dvef  25721  dvlipcn  25735  dvgt0lem2  25744  lhop1lem  25754  ftc1cn  25784  ftc2  25785  itgpowd  25791  deg1mul3le  25858  coeeulem  25962  dgrcolem1  26011  dgrcolem2  26012  plycpn  26026  dvntaylp  26107  pserdv  26165  pige3ALT  26253  cxpcn2  26478  rlimcnp3  26696  lgamgulmlem2  26758  basellem2  26810  pntrsumo1  27292  pntrsumbnd  27293  nosupbnd1lem1  27435  noinfbnd1lem1  27450  cutlt  27645  nbupgr  28856  nbumgrvtx  28858  nbgr2vtx1edg  28862  cusgrexilem2  28954  ifpsnprss  29135  1pthon2ve  29662  suppovss  32161  offinsupp1  32207  xrsmulgzz  32434  gsummpt2co  32458  gsumpart  32465  gsumhashmul  32466  symgcom2  32503  pmtrcnelor  32510  tocycfvres1  32527  tocycfvres2  32528  cycpmconjvlem  32558  fldgenid  32667  lindfpropd  32760  lsmsnpridl  32770  qusrn  32782  elrspunidl  32808  mxidlprm  32848  ssmxidl  32852  evls1fpws  32908  rlmdim  32970  rgmoddimOLD  32971  tngdim  32974  matdim  32976  ply1degltdimlem  32983  fedgmullem1  32990  algextdeglem8  33057  mdetpmtr1  33089  zarclssn  33139  zart0  33145  zarcmplem  33147  pnfneige0  33217  pwsiga  33414  baselcarsg  33591  efmul2picn  33894  reprfz1  33922  breprexplemc  33930  circlemeth  33938  circlevma  33940  circlemethhgt  33941  hgt750lemb  33954  hgt750lema  33955  hgt750leme  33956  tgoldbachgtde  33958  satfsschain  34641  mrsubff1  34791  mrsub0  34793  mrsubccat  34795  mrsubcn  34796  msubff1  34833  mthmpps  34859  wzel  35088  gg-dvcnp2  35460  gg-dvmulbr  35461  gg-dvcobr  35462  knoppndvlem6  35696  knoppndv  35713  bj-elpwg  36236  bj-restpw  36276  bj-restb  36278  bj-restuni2  36282  ftc1cnnclem  36862  ftc1cnnc  36863  ftc2nc  36873  areacirclem3  36881  welb  36907  cnresima  36935  rngoidl  37195  1psubclN  39118  cdlemefrs32fva  39574  lcmineqlem9  41208  lcmineqlem12  41211  intlewftc  41232  aks4d1p9  41259  sticksstones11  41278  mhmcompl  41422  evlsvvvallem  41435  evlsvvvallem2  41436  evlsvvval  41437  selvcllem4  41455  selvvvval  41459  evlselv  41461  addinvcom  41606  rgspnid  42216  oacl2g  42382  omabs2  42384  omcl2  42385  tfsconcatb0  42396  naddgeoa  42447  harval3  42591  cnvtrucl0  42677  brfvrtrcld  42787  clsk3nimkb  43093  k0004ss2  43205  extoimad  43218  mnuprd  43337  dvconstbi  43395  ssinc  44078  ssdec  44079  restopn3  44147  founiiun  44177  choicefi  44198  islptre  44634  fnlimfvre  44689  addccncf2  44891  fsumcncf  44893  cncfperiod  44894  negcncfg  44896  cncfuni  44901  icccncfext  44902  cncficcgt0  44903  fprodcncf  44915  dvcnre  44931  fperdvper  44934  itgsinexplem1  44969  itgcoscmulx  44984  smfpimne2  45855  rnghmsscmap2  46960  rhmsscmap2  47006  fldhmsubc  47071  fldhmsubcALTV  47089  elbigolo1  47331  sepfsepc  47648