Theorem ssidd 3982

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795

This theorem depends on definitions:  df-bi 207  df-ss 3943

This theorem is referenced by:  funfvima2d  7224  suppofss1d  8203  suppofss2d  8204  fpr1  8302  ralxpmap  8910  fissuni  9369  fsuppssov1  9396  fsuppmptif  9411  fsuppco2  9415  fsuppcor  9416  mapfienlem1  9417  mapfienlem2  9418  cantnfp1lem1  9692  cantnfp1lem3  9694  cantnflem1  9703  htalem  9910  ackbij2lem4  10255  cflim2  10277  fin23lem15  10348  wunex2  10752  swrd0  14676  rtrclreclem1  15076  summolem3  15730  isum  15735  fsumser  15746  fsumcl  15749  flo1  15870  prodmolem3  15949  iprod  15954  iprodn0  15956  fprodss  15964  fprodcl  15968  fprodclf  16008  rpnnen2lem11  16242  eulerthlem2  16801  mremre  17616  catsubcat  17852  yon11  18276  yon12  18277  yon2  18278  yonpropd  18280  oppcyon  18281  yonffth  18296  submgmid  18684  submid  18788  mulgnncl  19072  mulgnn0cl  19073  mulgcl  19074  subgid  19111  snsymgefmndeq  19376  symggen  19451  gsumzcl2  19891  gsumzf1o  19893  gsum2dlem1  19951  gsum2dlem2  19952  gsum2d  19953  gsumxp2  19961  dprdfinv  20002  dmdprdsplitlem  20020  dprd2db  20026  dpjidcl  20041  ablfac1eu  20056  ablfaclem2  20069  gsumdixp  20279  subrngid  20509  rnghmsscmap2  20589  rhmsscmap2  20618  fldhmsubc  20745  primefld  20765  lcomfsupp  20859  lss1  20895  rlmbas  21151  rlmplusg  21152  rlm0  21153  rlmmulr  21155  rlmsca  21156  rlmsca2  21157  rlmvsca  21158  rlmtopn  21159  rlmds  21160  rng2idl1cntr  21266  regsumsupp  21582  frlmsslsp  21756  frlmup1  21758  rnasclassa  21855  mplsubglem  21959  mpllsslem  21960  mplsubrglem  21964  mplcoe1  21995  mplcoe5  21998  mplbas2  22000  evlslem4  22034  psrbagev1  22035  evlslem2  22037  mhpvscacl  22092  psdmplcl  22100  evls1fpws  22307  evl1maprhm  22317  mhmcompl  22318  mamures  22335  cpmadumatpolylem2  22820  neiptopuni  23068  neiptoptop  23069  restopn2  23115  rncmp  23334  cmpfi  23346  conncn  23364  llyidm  23426  nllyidm  23427  toplly  23428  kgentopon  23476  kgencn2  23495  ptcld  23551  qtopuni  23640  supnfcls  23958  utopbas  24174  metustfbas  24496  rrxcph  25344  rrxmval  25357  rrxdstprj1  25361  evthicc2  25413  volcn  25559  dvres3  25866  dvres3a  25867  dvidlem  25868  dvmptresicc  25869  dvcnp2  25873  dvnadd  25883  dvnres  25885  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcmul  25899  dvcmulf  25900  dvcobr  25901  dvcobrOLD  25902  dvcjbr  25905  dvrec  25911  dveflem  25935  dvef  25936  dvlipcn  25951  dvgt0lem2  25960  lhop1lem  25970  ftc1cn  26002  ftc2  26003  itgpowd  26009  deg1mul3le  26074  coeeulem  26181  dgrcolem1  26231  dgrcolem2  26232  plycpn  26249  dvntaylp  26331  pserdv  26391  pige3ALT  26481  cxpcn2  26708  rlimcnp3  26929  lgamgulmlem2  26992  basellem2  27044  pntrsumo1  27528  pntrsumbnd  27529  nosupbnd1lem1  27672  noinfbnd1lem1  27687  cutlt  27892  nbupgr  29323  nbumgrvtx  29325  nbgr2vtx1edg  29329  cusgrexilem2  29421  ifpsnprss  29603  1pthon2ve  30135  suppovss  32658  offinsupp1  32704  xrsmulgzz  33001  gsummpt2co  33042  gsumfs2d  33049  gsumpart  33051  gsumhashmul  33055  symgcom2  33095  pmtrcnelor  33102  tocycfvres1  33121  tocycfvres2  33122  cycpmconjvlem  33152  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnsubrunlem1  33242  fracf1  33301  idomsubr  33303  fldgenid  33313  lindfpropd  33397  lsmsnpridl  33413  qusrn  33424  elrspunidl  33443  ssdifidl  33472  mxidlprm  33485  ssmxidl  33489  rlmdim  33649  rgmoddimOLD  33650  tngdim  33653  matdim  33655  ply1degltdimlem  33662  fedgmullem1  33669  fldextrspunlsplem  33714  algextdeglem8  33758  constrmon  33778  mdetpmtr1  33854  zarclssn  33904  zart0  33910  zarcmplem  33912  pnfneige0  33982  pwsiga  34161  baselcarsg  34338  boolesineq  34487  efmul2picn  34628  reprfz1  34656  breprexplemc  34664  circlemeth  34672  circlevma  34674  circlemethhgt  34675  hgt750lemb  34688  hgt750lema  34689  hgt750leme  34690  tgoldbachgtde  34692  satfsschain  35386  mrsubff1  35536  mrsub0  35538  mrsubccat  35540  mrsubcn  35541  msubff1  35578  mthmpps  35604  wzel  35842  knoppndvlem6  36535  knoppndv  36552  bj-elpwg  37070  bj-restpw  37110  bj-restb  37112  bj-restuni2  37116  ftc1cnnclem  37715  ftc1cnnc  37716  ftc2nc  37726  areacirclem3  37734  welb  37760  cnresima  37788  rngoidl  38048  1psubclN  39963  cdlemefrs32fva  40419  lcmineqlem9  42050  lcmineqlem12  42053  intlewftc  42074  aks4d1p9  42101  primrootspoweq0  42119  sticksstones11  42169  aks6d1c6lem3  42185  aks6d1c6lem4  42186  aks6d1c6lem5  42190  aks6d1c7lem1  42193  addinvcom  42474  evlsvvvallem  42584  evlsvvvallem2  42585  evlsvvval  42586  selvcllem4  42604  selvvvval  42608  evlselv  42610  rgspnid  43192  oacl2g  43354  omabs2  43356  omcl2  43357  tfsconcatb0  43368  naddgeoa  43418  harval3  43562  cnvtrucl0  43648  brfvrtrcld  43758  clsk3nimkb  44064  k0004ss2  44176  extoimad  44188  mnuprd  44300  dvconstbi  44358  ssinc  45111  ssdec  45112  restopn3  45175  founiiun  45203  choicefi  45224  islptre  45648  fnlimfvre  45703  addccncf2  45905  fsumcncf  45907  cncfperiod  45908  negcncfg  45910  cncfuni  45915  icccncfext  45916  cncficcgt0  45917  fprodcncf  45929  dvcnre  45945  fperdvper  45948  itgsinexplem1  45983  itgcoscmulx  45998  smfpimne2  46869  predgclnbgrel  47852  isubgrvtxuhgr  47877  fldhmsubcALTV  48308  elbigolo1  48537  iunlub  48799  iinglb  48800  sepfsepc  48902