Theorem ssidd 3958

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3902

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

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

This theorem is referenced by:  funfvima2d  7180  suppofss1d  8148  suppofss2d  8149  fpr1  8247  ralxpmap  8838  fissuni  9261  fsuppssov1  9291  fsuppmptif  9306  fsuppco2  9310  fsuppcor  9311  mapfienlem1  9312  mapfienlem2  9313  cantnfp1lem1  9591  cantnfp1lem3  9593  cantnflem1  9602  htalem  9812  ackbij2lem4  10155  cflim2  10177  fin23lem15  10248  wunex2  10653  swrd0  14586  rtrclreclem1  14984  summolem3  15641  isum  15646  fsumser  15657  fsumcl  15660  flo1  15781  prodmolem3  15860  iprod  15865  iprodn0  15867  fprodss  15875  fprodcl  15879  fprodclf  15919  rpnnen2lem11  16153  eulerthlem2  16713  mremre  17527  catsubcat  17767  yon11  18191  yon12  18192  yon2  18193  yonpropd  18195  oppcyon  18196  yonffth  18211  submgmid  18635  submid  18739  mulgnncl  19023  mulgnn0cl  19024  mulgcl  19025  subgid  19062  snsymgefmndeq  19328  symggen  19403  gsumzcl2  19843  gsumzf1o  19845  gsum2dlem1  19903  gsum2dlem2  19904  gsum2d  19905  gsumxp2  19913  dprdfinv  19954  dmdprdsplitlem  19972  dprd2db  19978  dpjidcl  19993  ablfac1eu  20008  ablfaclem2  20021  gsumdixp  20258  subrngid  20486  rnghmsscmap2  20566  rhmsscmap2  20595  fldhmsubc  20722  primefld  20742  lcomfsupp  20857  lss1  20893  rlmbas  21149  rlmplusg  21150  rlm0  21151  rlmmulr  21153  rlmsca  21154  rlmsca2  21155  rlmvsca  21156  rlmtopn  21157  rlmds  21158  rng2idl1cntr  21264  regsumsupp  21581  frlmsslsp  21755  frlmup1  21757  rnasclassa  21855  mplsubglem  21958  mpllsslem  21959  mplsubrglem  21963  mplcoe1  21996  mplcoe5  21999  mplbas2  22001  evlslem4  22035  psrbagev1  22036  evlslem2  22038  evlsvvvallem  22050  evlsvvvallem2  22051  evlsvvval  22052  mhpvscacl  22101  psdmplcl  22109  evls1fpws  22317  evl1maprhm  22327  mhmcompl  22328  mamures  22345  cpmadumatpolylem2  22830  neiptopuni  23078  neiptoptop  23079  restopn2  23125  rncmp  23344  cmpfi  23356  conncn  23374  llyidm  23436  nllyidm  23437  toplly  23438  kgentopon  23486  kgencn2  23505  ptcld  23561  qtopuni  23650  supnfcls  23968  utopbas  24183  metustfbas  24505  rrxcph  25352  rrxmval  25365  rrxdstprj1  25369  evthicc2  25421  volcn  25567  dvres3  25874  dvres3a  25875  dvidlem  25876  dvmptresicc  25877  dvcnp2  25881  dvnadd  25891  dvnres  25893  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcmul  25907  dvcmulf  25908  dvcobr  25909  dvcobrOLD  25910  dvcjbr  25913  dvrec  25919  dveflem  25943  dvef  25944  dvlipcn  25959  dvgt0lem2  25968  lhop1lem  25978  ftc1cn  26010  ftc2  26011  itgpowd  26017  deg1mul3le  26082  coeeulem  26189  dgrcolem1  26239  dgrcolem2  26240  plycpn  26257  dvntaylp  26339  pserdv  26399  pige3ALT  26489  cxpcn2  26716  rlimcnp3  26937  lgamgulmlem2  27000  basellem2  27052  pntrsumo1  27536  pntrsumbnd  27537  nosupbnd1lem1  27680  noinfbnd1lem1  27695  cutlt  27914  nbupgr  29400  nbumgrvtx  29402  nbgr2vtx1edg  29406  cusgrexilem2  29498  ifpsnprss  29679  1pthon2ve  30212  suppovss  32741  offinsupp1  32786  xrsmulgzz  33072  gsummpt2co  33112  gsummptrev  33120  gsummptp1  33121  gsumfs2d  33125  gsumpart  33127  gsumhashmul  33131  gsummulsubdishift1  33132  symgcom2  33147  pmtrcnelor  33154  tocycfvres1  33173  tocycfvres2  33174  cycpmconjvlem  33204  elrgspnlem1  33305  elrgspnlem2  33306  elrgspnsubrunlem1  33310  fracf1  33370  idomsubr  33372  fldgenid  33382  lindfpropd  33444  lsmsnpridl  33460  qusrn  33471  elrspunidl  33490  ssdifidl  33519  mxidlprm  33532  ssmxidl  33536  evlextv  33688  mplvrpmrhm  33693  vieta  33717  srapwov  33726  rlmdim  33747  rgmoddimOLD  33748  tngdim  33751  matdim  33753  ply1degltdimlem  33760  fedgmullem1  33767  fldextrspunlsplem  33811  algextdeglem8  33862  constrmon  33882  mdetpmtr1  33961  zarclssn  34011  zart0  34017  zarcmplem  34019  pnfneige0  34089  pwsiga  34268  baselcarsg  34444  boolesineq  34593  efmul2picn  34734  reprfz1  34762  breprexplemc  34770  circlemeth  34778  circlevma  34780  circlemethhgt  34781  hgt750lemb  34794  hgt750lema  34795  hgt750leme  34796  tgoldbachgtde  34798  satfsschain  35539  mrsubff1  35689  mrsub0  35691  mrsubccat  35693  mrsubcn  35694  msubff1  35731  mthmpps  35757  wzel  35997  knoppndvlem6  36692  knoppndv  36709  bj-elpwg  37228  bj-restpw  37268  bj-restb  37270  bj-restuni2  37274  ftc1cnnclem  37863  ftc1cnnc  37864  ftc2nc  37874  areacirclem3  37882  welb  37908  cnresima  37936  rngoidl  38196  1psubclN  40241  cdlemefrs32fva  40697  lcmineqlem9  42328  lcmineqlem12  42331  intlewftc  42352  aks4d1p9  42379  primrootspoweq0  42397  sticksstones11  42447  aks6d1c6lem3  42463  aks6d1c6lem4  42464  aks6d1c6lem5  42468  aks6d1c7lem1  42471  addinvcom  42723  selvcllem4  42860  selvvvval  42864  evlselv  42866  rgspnid  43446  oacl2g  43608  omabs2  43610  omcl2  43611  tfsconcatb0  43622  naddgeoa  43672  harval3  43815  cnvtrucl0  43901  brfvrtrcld  44011  clsk3nimkb  44317  k0004ss2  44429  extoimad  44441  mnuprd  44553  dvconstbi  44611  ssinc  45367  ssdec  45368  restopn3  45431  founiiun  45459  choicefi  45480  islptre  45901  fnlimfvre  45954  addccncf2  46156  fsumcncf  46158  cncfperiod  46159  negcncfg  46161  cncfuni  46166  icccncfext  46167  cncficcgt0  46168  fprodcncf  46180  dvcnre  46196  fperdvper  46199  itgsinexplem1  46234  itgcoscmulx  46249  smfpimne2  47120  predgclnbgrel  48121  isubgrvtxuhgr  48146  fldhmsubcALTV  48615  elbigolo1  48839  iunlub  49102  iinglb  49103  sepfsepc  49209