Theorem ssidd 3970

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3914

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 3931

This theorem is referenced by:  funfvima2d  7206  suppofss1d  8183  suppofss2d  8184  fpr1  8282  ralxpmap  8869  fissuni  9308  fsuppssov1  9335  fsuppmptif  9350  fsuppco2  9354  fsuppcor  9355  mapfienlem1  9356  mapfienlem2  9357  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnflem1  9642  htalem  9849  ackbij2lem4  10194  cflim2  10216  fin23lem15  10287  wunex2  10691  swrd0  14623  rtrclreclem1  15023  summolem3  15680  isum  15685  fsumser  15696  fsumcl  15699  flo1  15820  prodmolem3  15899  iprod  15904  iprodn0  15906  fprodss  15914  fprodcl  15918  fprodclf  15958  rpnnen2lem11  16192  eulerthlem2  16752  mremre  17565  catsubcat  17801  yon11  18225  yon12  18226  yon2  18227  yonpropd  18229  oppcyon  18230  yonffth  18245  submgmid  18633  submid  18737  mulgnncl  19021  mulgnn0cl  19022  mulgcl  19023  subgid  19060  snsymgefmndeq  19325  symggen  19400  gsumzcl2  19840  gsumzf1o  19842  gsum2dlem1  19900  gsum2dlem2  19901  gsum2d  19902  gsumxp2  19910  dprdfinv  19951  dmdprdsplitlem  19969  dprd2db  19975  dpjidcl  19990  ablfac1eu  20005  ablfaclem2  20018  gsumdixp  20228  subrngid  20458  rnghmsscmap2  20538  rhmsscmap2  20567  fldhmsubc  20694  primefld  20714  lcomfsupp  20808  lss1  20844  rlmbas  21100  rlmplusg  21101  rlm0  21102  rlmmulr  21104  rlmsca  21105  rlmsca2  21106  rlmvsca  21107  rlmtopn  21108  rlmds  21109  rng2idl1cntr  21215  regsumsupp  21531  frlmsslsp  21705  frlmup1  21707  rnasclassa  21804  mplsubglem  21908  mpllsslem  21909  mplsubrglem  21913  mplcoe1  21944  mplcoe5  21947  mplbas2  21949  evlslem4  21983  psrbagev1  21984  evlslem2  21986  mhpvscacl  22041  psdmplcl  22049  evls1fpws  22256  evl1maprhm  22266  mhmcompl  22267  mamures  22284  cpmadumatpolylem2  22769  neiptopuni  23017  neiptoptop  23018  restopn2  23064  rncmp  23283  cmpfi  23295  conncn  23313  llyidm  23375  nllyidm  23376  toplly  23377  kgentopon  23425  kgencn2  23444  ptcld  23500  qtopuni  23589  supnfcls  23907  utopbas  24123  metustfbas  24445  rrxcph  25292  rrxmval  25305  rrxdstprj1  25309  evthicc2  25361  volcn  25507  dvres3  25814  dvres3a  25815  dvidlem  25816  dvmptresicc  25817  dvcnp2  25821  dvnadd  25831  dvnres  25833  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmul  25847  dvcmulf  25848  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvrec  25859  dveflem  25883  dvef  25884  dvlipcn  25899  dvgt0lem2  25908  lhop1lem  25918  ftc1cn  25950  ftc2  25951  itgpowd  25957  deg1mul3le  26022  coeeulem  26129  dgrcolem1  26179  dgrcolem2  26180  plycpn  26197  dvntaylp  26279  pserdv  26339  pige3ALT  26429  cxpcn2  26656  rlimcnp3  26877  lgamgulmlem2  26940  basellem2  26992  pntrsumo1  27476  pntrsumbnd  27477  nosupbnd1lem1  27620  noinfbnd1lem1  27635  cutlt  27840  nbupgr  29271  nbumgrvtx  29273  nbgr2vtx1edg  29277  cusgrexilem2  29369  ifpsnprss  29551  1pthon2ve  30083  suppovss  32604  offinsupp1  32650  xrsmulgzz  32947  gsummpt2co  32988  gsumfs2d  32995  gsumpart  32997  gsumhashmul  33001  symgcom2  33041  pmtrcnelor  33048  tocycfvres1  33067  tocycfvres2  33068  cycpmconjvlem  33098  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnsubrunlem1  33198  fracf1  33257  idomsubr  33259  fldgenid  33269  lindfpropd  33353  lsmsnpridl  33369  qusrn  33380  elrspunidl  33399  ssdifidl  33428  mxidlprm  33441  ssmxidl  33445  rlmdim  33605  rgmoddimOLD  33606  tngdim  33609  matdim  33611  ply1degltdimlem  33618  fedgmullem1  33625  fldextrspunlsplem  33668  algextdeglem8  33714  constrmon  33734  mdetpmtr1  33813  zarclssn  33863  zart0  33869  zarcmplem  33871  pnfneige0  33941  pwsiga  34120  baselcarsg  34297  boolesineq  34446  efmul2picn  34587  reprfz1  34615  breprexplemc  34623  circlemeth  34631  circlevma  34633  circlemethhgt  34634  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  satfsschain  35351  mrsubff1  35501  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  msubff1  35543  mthmpps  35569  wzel  35812  knoppndvlem6  36505  knoppndv  36522  bj-elpwg  37040  bj-restpw  37080  bj-restb  37082  bj-restuni2  37086  ftc1cnnclem  37685  ftc1cnnc  37686  ftc2nc  37696  areacirclem3  37704  welb  37730  cnresima  37758  rngoidl  38018  1psubclN  39938  cdlemefrs32fva  40394  lcmineqlem9  42025  lcmineqlem12  42028  intlewftc  42049  aks4d1p9  42076  primrootspoweq0  42094  sticksstones11  42144  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6lem5  42165  aks6d1c7lem1  42168  addinvcom  42420  evlsvvvallem  42549  evlsvvvallem2  42550  evlsvvval  42551  selvcllem4  42569  selvvvval  42573  evlselv  42575  rgspnid  43157  oacl2g  43319  omabs2  43321  omcl2  43322  tfsconcatb0  43333  naddgeoa  43383  harval3  43527  cnvtrucl0  43613  brfvrtrcld  43723  clsk3nimkb  44029  k0004ss2  44141  extoimad  44153  mnuprd  44265  dvconstbi  44323  ssinc  45081  ssdec  45082  restopn3  45145  founiiun  45173  choicefi  45194  islptre  45617  fnlimfvre  45672  addccncf2  45874  fsumcncf  45876  cncfperiod  45877  negcncfg  45879  cncfuni  45884  icccncfext  45885  cncficcgt0  45886  fprodcncf  45898  dvcnre  45914  fperdvper  45917  itgsinexplem1  45952  itgcoscmulx  45967  smfpimne2  46838  predgclnbgrel  47839  isubgrvtxuhgr  47864  fldhmsubcALTV  48321  elbigolo1  48546  iunlub  48809  iinglb  48810  sepfsepc  48916