Theorem ssidd 3953

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ss 3915

This theorem is used by:  pwidg  4576  funfvima2d  7226  suppofss1d  8199  suppofss2d  8200  fpr1  8299  ralxpmap  8902  fissuni  9324  fsuppssov1  9354  fsuppmptif  9369  fsuppco2  9373  fsuppcor  9374  mapfienlem1  9375  mapfienlem2  9376  cantnfp1lem1  9657  cantnfp1lem3  9659  cantnflem1  9668  htalem  9933  ackbij2lem4  10291  cflim2  10313  fin23lem15  10384  wunex2  10795  swrd0  14776  rtrclreclem1  15178  summolem3  15848  isum  15853  fsumser  15864  fsumcl  15867  flo1  15991  prodmolem3  16068  iprod  16073  iprodn0  16075  fprodss  16083  fprodcl  16087  fprodclf  16127  rpnnen2lem11  16360  eulerthlem2  16921  mremre  17736  catsubcat  17976  yon11  18400  yon12  18401  yon2  18402  yonpropd  18404  oppcyon  18405  yonffth  18420  submgmid  18857  submid  18967  mulgnncl  19261  mulgnn0cl  19262  mulgcl  19263  subgid  19300  snsymgefmndeq  19571  symggen  19646  gsumzcl2  20086  gsumzf1o  20088  gsum2dlem1  20146  gsum2dlem2  20147  gsum2d  20148  gsumxp2  20156  dprdfinv  20197  dmdprdsplitlem  20215  dprd2db  20221  dpjidcl  20236  ablfac1eu  20251  ablfaclem2  20264  gsumdixp  20510  subrngid  20763  rnghmsscmap2  20843  rhmsscmap2  20872  fldhmsubc  21004  primefld  21024  lcomfsupp  21139  lss1  21175  rlmbas  21430  rlmplusg  21431  rlm0  21432  rlmmulr  21434  rlmsca  21435  rlmsca2  21436  rlmvsca  21437  rlmtopn  21438  rlmds  21439  rng2idl1cntr  21563  ssdifidl  21603  regsumsupp  21890  frlmsslsp  22064  frlmup1  22066  rnasclassa  22165  mplsubglem  22268  mpllsslem  22269  mplsubrglem  22273  mplcoe1  22308  mplcoe5  22311  mplbas2  22313  evlslem4  22347  psrbagev1  22348  evlslem2  22350  evlsvvvallem  22362  evlsvvvallem2  22363  evlsvvval  22364  mhmcompl  22392  selvcllem4  22409  selvvvval  22413  mhpvscacl  22437  psdmplcl  22445  evls1fpws  22649  evl1maprhm  22659  mamures  22674  cpmadumatpolylem2  23162  neiptopuni  23410  neiptoptop  23411  restopn2  23457  rncmp  23676  cmpfi  23688  conncn  23706  llyidm  23769  nllyidm  23770  toplly  23771  kgentopon  23819  kgencn2  23838  ptcld  23894  qtopuni  23983  supnfcls  24301  utopbas  24516  metustfbas  24838  rrxcph  25675  rrxmval  25688  rrxdstprj1  25692  evthicc2  25743  volcn  25889  dvres3  26195  dvres3a  26196  dvidlem  26197  dvmptresicc  26198  dvcnp2  26202  dvnadd  26211  dvnres  26213  dvaddbr  26220  dvmulbr  26221  dvcmul  26226  dvcmulf  26227  dvcobr  26228  dvcjbr  26231  dvrec  26237  dveflem  26261  dvef  26262  dvlipcn  26276  dvgt0lem2  26285  lhop1lem  26295  ftc1cn  26325  ftc2  26326  itgpowd  26332  deg1mul3le  26397  coeeulem  26505  dgrcolem1  26554  dgrcolem2  26555  plycpn  26574  rnplynfin  26594  dvntaylp  26662  pserdv  26720  pige3ALT  26812  cxpcn2  27038  rlimcnp3  27259  lgamgulmlem2  27321  basellem2  27373  pntrsumo1  27856  pntrsumbnd  27857  nosupbnd1lem1  27999  noinfbnd1lem1  28014  cutlt  28252  nbupgr  29859  nbumgrvtx  29861  nbgr2vtx1edg  29865  cusgrexilem2  29957  ifpsnprss  30137  1pthon2ve  30689  suppovss  33208  offinsupp1  33252  xrsmulgzz  33504  gsummpt2co  33543  gsummptrev  33551  gsummptp1  33552  gsumfs2d  33556  gsumpart  33558  gsumhashmul  33562  gsummulsubdishift1  33563  symgcom2  33579  pmtrcnelor  33586  tocycfvres1  33605  tocycfvres2  33606  cycpmconjvlem  33636  elrgspnlem1  33737  elrgspnlem2  33738  elrgspnsubrunlem1  33742  fracf1  33803  idomsubr  33805  fldgenid  33815  lindfpropd  33871  lsmsnpridl  33885  qusrn  33894  elrspunidl  33912  mxidlprm  33929  ssmxidl  33933  selvply1rhmlemb  34085  evlextv  34108  mplvrpmrhm  34113  vieta  34146  srapwov  34155  rlmdim  34176  tngdim  34179  matdim  34181  ply1degltdimlem  34188  fedgmullem1  34195  fldextrspunlsplem  34239  algextdeglem8  34290  constrmon  34310  mdetpmtr1  34389  zarclssn  34439  zart0  34445  zarcmplem  34447  pnfneige0  34517  pwsiga  34696  baselcarsg  34873  boolesineq  35022  efmul2picn  35160  reprfz1  35188  breprexplemc  35196  circlemeth  35204  circlevma  35206  circlemethhgt  35207  hgt750lemb  35220  hgt750lema  35221  hgt750leme  35222  tgoldbachgtde  35224  satfsschain  36050  mrsubff1  36200  mrsub0  36202  mrsubccat  36204  mrsubcn  36205  msubff1  36242  mthmpps  36268  wzel  36508  nmulprop  36861  knoppndvlem6  37305  knoppndv  37322  bj-elpwg  37887  bj-restpw  37933  bj-restb  37935  bj-restuni2  37939  ftc1cnnclem  38529  ftc1cnnc  38530  ftc2nc  38540  areacirclem3  38548  welb  38590  cnresima  38618  rngoidl  38878  1psubclN  40921  cdlemefrs32fva  41377  lcmineqlem9  43007  lcmineqlem12  43010  intlewftc  43031  aks4d1p9  43058  primrootspoweq0  43076  sticksstones11  43126  aks6d1c6lem3  43142  aks6d1c6lem4  43143  aks6d1c6lem5  43147  aks6d1c7lem1  43150  addinvcom  43411  evlselv  43539  rgspnid  44113  oacl2g  44275  omabs2  44277  omcl2  44278  tfsconcatb0  44289  naddgeoa  44339  harval3  44482  cnvtrucl0  44568  brfvrtrcld  44678  clsk3nimkb  44984  k0004ss2  45096  extoimad  45108  mnuprd  45204  dvconstbi  45262  ssinc  46023  ssdec  46024  restopn3  46087  founiiun  46115  choicefi  46135  islptre  46553  fnlimfvre  46606  addccncf2  46808  fsumcncf  46810  cncfperiod  46811  negcncfg  46813  cncfuni  46818  icccncfext  46819  cncficcgt0  46820  fprodcncf  46832  dvcnre  46848  fperdvper  46851  itgsinexplem1  46886  itgcoscmulx  46901  fourierdlem113  47151  smfpimne2  47772  predgclnbgrel  48859  isubgrvtxuhgr  48884  fldhmsubcALTV  49352  elbigolo1  49591  iunlub  49853  iinglb  49854  sepfsepc  49958