Theorem ssidd 3955

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3899

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

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

This theorem is referenced by:  funfvima2d  7175  suppofss1d  8143  suppofss2d  8144  fpr1  8242  ralxpmap  8829  fissuni  9251  fsuppssov1  9278  fsuppmptif  9293  fsuppco2  9297  fsuppcor  9298  mapfienlem1  9299  mapfienlem2  9300  cantnfp1lem1  9578  cantnfp1lem3  9580  cantnflem1  9589  htalem  9799  ackbij2lem4  10142  cflim2  10164  fin23lem15  10235  wunex2  10639  swrd0  14576  rtrclreclem1  14974  summolem3  15631  isum  15636  fsumser  15647  fsumcl  15650  flo1  15771  prodmolem3  15850  iprod  15855  iprodn0  15857  fprodss  15865  fprodcl  15869  fprodclf  15909  rpnnen2lem11  16143  eulerthlem2  16703  mremre  17516  catsubcat  17756  yon11  18180  yon12  18181  yon2  18182  yonpropd  18184  oppcyon  18185  yonffth  18200  submgmid  18624  submid  18728  mulgnncl  19012  mulgnn0cl  19013  mulgcl  19014  subgid  19051  snsymgefmndeq  19317  symggen  19392  gsumzcl2  19832  gsumzf1o  19834  gsum2dlem1  19892  gsum2dlem2  19893  gsum2d  19894  gsumxp2  19902  dprdfinv  19943  dmdprdsplitlem  19961  dprd2db  19967  dpjidcl  19982  ablfac1eu  19997  ablfaclem2  20010  gsumdixp  20247  subrngid  20474  rnghmsscmap2  20554  rhmsscmap2  20583  fldhmsubc  20710  primefld  20730  lcomfsupp  20845  lss1  20881  rlmbas  21137  rlmplusg  21138  rlm0  21139  rlmmulr  21141  rlmsca  21142  rlmsca2  21143  rlmvsca  21144  rlmtopn  21145  rlmds  21146  rng2idl1cntr  21252  regsumsupp  21569  frlmsslsp  21743  frlmup1  21745  rnasclassa  21842  mplsubglem  21946  mpllsslem  21947  mplsubrglem  21951  mplcoe1  21982  mplcoe5  21985  mplbas2  21987  evlslem4  22021  psrbagev1  22022  evlslem2  22024  mhpvscacl  22079  psdmplcl  22087  evls1fpws  22294  evl1maprhm  22304  mhmcompl  22305  mamures  22322  cpmadumatpolylem2  22807  neiptopuni  23055  neiptoptop  23056  restopn2  23102  rncmp  23321  cmpfi  23333  conncn  23351  llyidm  23413  nllyidm  23414  toplly  23415  kgentopon  23463  kgencn2  23482  ptcld  23538  qtopuni  23627  supnfcls  23945  utopbas  24160  metustfbas  24482  rrxcph  25329  rrxmval  25342  rrxdstprj1  25346  evthicc2  25398  volcn  25544  dvres3  25851  dvres3a  25852  dvidlem  25853  dvmptresicc  25854  dvcnp2  25858  dvnadd  25868  dvnres  25870  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  dvcmul  25884  dvcmulf  25885  dvcobr  25886  dvcobrOLD  25887  dvcjbr  25890  dvrec  25896  dveflem  25920  dvef  25921  dvlipcn  25936  dvgt0lem2  25945  lhop1lem  25955  ftc1cn  25987  ftc2  25988  itgpowd  25994  deg1mul3le  26059  coeeulem  26166  dgrcolem1  26216  dgrcolem2  26217  plycpn  26234  dvntaylp  26316  pserdv  26376  pige3ALT  26466  cxpcn2  26693  rlimcnp3  26914  lgamgulmlem2  26977  basellem2  27029  pntrsumo1  27513  pntrsumbnd  27514  nosupbnd1lem1  27657  noinfbnd1lem1  27672  cutlt  27886  nbupgr  29333  nbumgrvtx  29335  nbgr2vtx1edg  29339  cusgrexilem2  29431  ifpsnprss  29612  1pthon2ve  30145  suppovss  32673  offinsupp1  32720  xrsmulgzz  33001  gsummpt2co  33039  gsumfs2d  33046  gsumpart  33048  gsumhashmul  33052  symgcom2  33064  pmtrcnelor  33071  tocycfvres1  33090  tocycfvres2  33091  cycpmconjvlem  33121  elrgspnlem1  33220  elrgspnlem2  33221  elrgspnsubrunlem1  33225  fracf1  33284  idomsubr  33286  fldgenid  33296  lindfpropd  33358  lsmsnpridl  33374  qusrn  33385  elrspunidl  33404  ssdifidl  33433  mxidlprm  33446  ssmxidl  33450  mplvrpmrhm  33588  srapwov  33612  rlmdim  33633  rgmoddimOLD  33634  tngdim  33637  matdim  33639  ply1degltdimlem  33646  fedgmullem1  33653  fldextrspunlsplem  33697  algextdeglem8  33748  constrmon  33768  mdetpmtr1  33847  zarclssn  33897  zart0  33903  zarcmplem  33905  pnfneige0  33975  pwsiga  34154  baselcarsg  34330  boolesineq  34479  efmul2picn  34620  reprfz1  34648  breprexplemc  34656  circlemeth  34664  circlevma  34666  circlemethhgt  34667  hgt750lemb  34680  hgt750lema  34681  hgt750leme  34682  tgoldbachgtde  34684  satfsschain  35419  mrsubff1  35569  mrsub0  35571  mrsubccat  35573  mrsubcn  35574  msubff1  35611  mthmpps  35637  wzel  35877  knoppndvlem6  36572  knoppndv  36589  bj-elpwg  37107  bj-restpw  37147  bj-restb  37149  bj-restuni2  37153  ftc1cnnclem  37741  ftc1cnnc  37742  ftc2nc  37752  areacirclem3  37760  welb  37786  cnresima  37814  rngoidl  38074  1psubclN  40053  cdlemefrs32fva  40509  lcmineqlem9  42140  lcmineqlem12  42143  intlewftc  42164  aks4d1p9  42191  primrootspoweq0  42209  sticksstones11  42259  aks6d1c6lem3  42275  aks6d1c6lem4  42276  aks6d1c6lem5  42280  aks6d1c7lem1  42283  addinvcom  42540  evlsvvvallem  42669  evlsvvvallem2  42670  evlsvvval  42671  selvcllem4  42689  selvvvval  42693  evlselv  42695  rgspnid  43275  oacl2g  43437  omabs2  43439  omcl2  43440  tfsconcatb0  43451  naddgeoa  43501  harval3  43645  cnvtrucl0  43731  brfvrtrcld  43841  clsk3nimkb  44147  k0004ss2  44259  extoimad  44271  mnuprd  44383  dvconstbi  44441  ssinc  45198  ssdec  45199  restopn3  45262  founiiun  45290  choicefi  45311  islptre  45733  fnlimfvre  45786  addccncf2  45988  fsumcncf  45990  cncfperiod  45991  negcncfg  45993  cncfuni  45998  icccncfext  45999  cncficcgt0  46000  fprodcncf  46012  dvcnre  46028  fperdvper  46031  itgsinexplem1  46066  itgcoscmulx  46081  smfpimne2  46952  predgclnbgrel  47953  isubgrvtxuhgr  47978  fldhmsubcALTV  48447  elbigolo1  48672  iunlub  48935  iinglb  48936  sepfsepc  49042