Theorem ssidd 3959

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

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

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

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

This theorem is used by:  pwidg  4581  funfvima2d  7230  suppofss1d  8198  suppofss2d  8199  fpr1  8298  ralxpmap  8892  fissuni  9312  fsuppssov1  9342  fsuppmptif  9357  fsuppco2  9361  fsuppcor  9362  mapfienlem1  9363  mapfienlem2  9364  cantnfp1lem1  9645  cantnfp1lem3  9647  cantnflem1  9656  htalem  9888  ackbij2lem4  10231  cflim2  10253  fin23lem15  10324  wunex2  10729  swrd0  14703  rtrclreclem1  15101  summolem3  15772  isum  15777  fsumser  15788  fsumcl  15791  flo1  15915  prodmolem3  15994  iprod  15999  iprodn0  16001  fprodss  16009  fprodcl  16013  fprodclf  16053  rpnnen2lem11  16286  eulerthlem2  16847  mremre  17662  catsubcat  17902  yon11  18326  yon12  18327  yon2  18328  yonpropd  18330  oppcyon  18331  yonffth  18346  submgmid  18770  submid  18874  mulgnncl  19161  mulgnn0cl  19162  mulgcl  19163  subgid  19200  snsymgefmndeq  19471  symggen  19546  gsumzcl2  19986  gsumzf1o  19988  gsum2dlem1  20046  gsum2dlem2  20047  gsum2d  20048  gsumxp2  20056  dprdfinv  20097  dmdprdsplitlem  20115  dprd2db  20121  dpjidcl  20136  ablfac1eu  20151  ablfaclem2  20164  gsumdixp  20407  subrngid  20659  rnghmsscmap2  20739  rhmsscmap2  20768  fldhmsubc  20899  primefld  20919  lcomfsupp  21034  lss1  21070  rlmbas  21325  rlmplusg  21326  rlm0  21327  rlmmulr  21329  rlmsca  21330  rlmsca2  21331  rlmvsca  21332  rlmtopn  21333  rlmds  21334  rng2idl1cntr  21456  ssdifidl  21496  regsumsupp  21783  frlmsslsp  21957  frlmup1  21959  rnasclassa  22056  mplsubglem  22159  mpllsslem  22160  mplsubrglem  22164  mplcoe1  22199  mplcoe5  22202  mplbas2  22204  evlslem4  22238  psrbagev1  22239  evlslem2  22241  evlsvvvallem  22253  evlsvvvallem2  22254  evlsvvval  22255  mhmcompl  22283  selvcllem4  22300  selvvvval  22304  mhpvscacl  22328  psdmplcl  22336  evls1fpws  22540  evl1maprhm  22550  mamures  22565  cpmadumatpolylem2  23050  neiptopuni  23298  neiptoptop  23299  restopn2  23345  rncmp  23564  cmpfi  23576  conncn  23594  llyidm  23656  nllyidm  23657  toplly  23658  kgentopon  23706  kgencn2  23725  ptcld  23781  qtopuni  23870  supnfcls  24188  utopbas  24403  metustfbas  24725  rrxcph  25562  rrxmval  25575  rrxdstprj1  25579  evthicc2  25630  volcn  25776  dvres3  26083  dvres3a  26084  dvidlem  26085  dvmptresicc  26086  dvcnp2  26090  dvnadd  26099  dvnres  26101  dvaddbr  26108  dvmulbr  26109  dvcmul  26114  dvcmulf  26115  dvcobr  26116  dvcjbr  26119  dvrec  26125  dveflem  26149  dvef  26150  dvlipcn  26164  dvgt0lem2  26173  lhop1lem  26183  ftc1cn  26213  ftc2  26214  itgpowd  26220  deg1mul3le  26285  coeeulem  26392  dgrcolem1  26441  dgrcolem2  26442  plycpn  26461  dvntaylp  26545  pserdv  26603  pige3ALT  26696  cxpcn2  26922  rlimcnp3  27143  lgamgulmlem2  27205  basellem2  27257  pntrsumo1  27740  pntrsumbnd  27741  nosupbnd1lem1  27883  noinfbnd1lem1  27898  cutlt  28136  nbupgr  29705  nbumgrvtx  29707  nbgr2vtx1edg  29711  cusgrexilem2  29803  ifpsnprss  29983  1pthon2ve  30516  suppovss  33037  offinsupp1  33082  xrsmulgzz  33338  gsummpt2co  33377  gsummptrev  33385  gsummptp1  33386  gsumfs2d  33390  gsumpart  33392  gsumhashmul  33396  gsummulsubdishift1  33397  symgcom2  33413  pmtrcnelor  33420  tocycfvres1  33439  tocycfvres2  33440  cycpmconjvlem  33470  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnsubrunlem1  33576  fracf1  33637  idomsubr  33639  fldgenid  33649  lindfpropd  33704  lsmsnpridl  33718  qusrn  33727  elrspunidl  33745  mxidlprm  33762  ssmxidl  33766  selvply1rhmlemb  33918  evlextv  33941  mplvrpmrhm  33946  vieta  33979  srapwov  33988  rlmdim  34009  tngdim  34012  matdim  34014  ply1degltdimlem  34021  fedgmullem1  34028  fldextrspunlsplem  34072  algextdeglem8  34123  constrmon  34143  mdetpmtr1  34222  zarclssn  34272  zart0  34278  zarcmplem  34280  pnfneige0  34350  pwsiga  34529  baselcarsg  34705  boolesineq  34854  efmul2picn  34992  reprfz1  35020  breprexplemc  35028  circlemeth  35036  circlevma  35038  circlemethhgt  35039  hgt750lemb  35052  hgt750lema  35053  hgt750leme  35054  tgoldbachgtde  35056  satfsschain  35864  mrsubff1  36014  mrsub0  36016  mrsubccat  36018  mrsubcn  36019  msubff1  36056  mthmpps  36082  wzel  36322  nmulprop  36690  knoppndvlem6  37134  knoppndv  37151  bj-elpwg  37716  bj-restpw  37762  bj-restb  37764  bj-restuni2  37768  ftc1cnnclem  38370  ftc1cnnc  38371  ftc2nc  38381  areacirclem3  38389  welb  38415  cnresima  38443  rngoidl  38703  1psubclN  40746  cdlemefrs32fva  41202  lcmineqlem9  42832  lcmineqlem12  42835  intlewftc  42856  aks4d1p9  42883  primrootspoweq0  42901  sticksstones11  42951  aks6d1c6lem3  42967  aks6d1c6lem4  42968  aks6d1c6lem5  42972  aks6d1c7lem1  42975  addinvcom  43221  evlselv  43349  rgspnid  43923  oacl2g  44085  omabs2  44087  omcl2  44088  tfsconcatb0  44099  naddgeoa  44149  harval3  44292  cnvtrucl0  44378  brfvrtrcld  44488  clsk3nimkb  44794  k0004ss2  44906  extoimad  44918  mnuprd  45014  dvconstbi  45072  ssinc  45833  ssdec  45834  restopn3  45897  founiiun  45925  choicefi  45945  islptre  46363  fnlimfvre  46416  addccncf2  46618  fsumcncf  46620  cncfperiod  46621  negcncfg  46623  cncfuni  46628  icccncfext  46629  cncficcgt0  46630  fprodcncf  46642  dvcnre  46658  fperdvper  46661  itgsinexplem1  46696  itgcoscmulx  46711  fourierdlem113  46961  smfpimne2  47582  predgclnbgrel  48632  isubgrvtxuhgr  48657  fldhmsubcALTV  49126  elbigolo1  49365  iunlub  49627  iinglb  49628  sepfsepc  49734