Theorem ssidd 3936

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

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

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 3901

This theorem is used by:  pwidg  4581  funfvima2d  7261  suppofss1d  8249  suppofss2d  8250  fpr1  8349  ralxpmap  8952  fissuni  9374  fsuppssov1  9403  fsuppmptif  9418  fsuppco2  9422  fsuppcor  9423  mapfienlem1  9424  mapfienlem2  9425  cantnfp1lem1  9706  cantnfp1lem3  9708  cantnflem1  9717  htalem  9988  ackbij2lem4  10346  cflim2  10368  fin23lem15  10439  wunex2  10850  swrd0  14836  rtrclreclem1  15239  summolem3  15909  isum  15914  fsumser  15925  fsumcl  15928  flo1  16052  prodmolem3  16129  iprod  16134  iprodn0  16136  fprodss  16144  fprodcl  16148  fprodclf  16188  rpnnen2lem11  16421  eulerthlem2  16988  mremre  17803  catsubcat  18043  yon11  18467  yon12  18468  yon2  18469  yonpropd  18471  oppcyon  18472  yonffth  18487  submgmid  18924  submid  19034  mulgnncl  19328  mulgnn0cl  19329  mulgcl  19330  subgid  19367  snsymgefmndeq  19639  symggen  19714  gsumzcl2  20154  gsumzf1o  20156  gsum2dlem1  20214  gsum2dlem2  20215  gsum2d  20216  gsumxp2  20224  dprdfinv  20265  dmdprdsplitlem  20283  dprd2db  20289  dpjidcl  20304  ablfac1eu  20319  ablfaclem2  20332  gsumdixp  20578  subrngid  20831  rnghmsscmap2  20911  rhmsscmap2  20940  fldhmsubc  21072  primefld  21092  lcomfsupp  21207  lss1  21243  rlmbas  21498  rlmplusg  21499  rlm0  21500  rlmmulr  21502  rlmsca  21503  rlmsca2  21504  rlmvsca  21505  rlmtopn  21506  rlmds  21507  rng2idl1cntr  21631  ssdifidl  21671  regsumsupp  21958  frlmsslsp  22132  frlmup1  22134  rnasclassa  22233  mplsubglem  22336  mpllsslem  22337  mplsubrglem  22341  mplcoe1  22376  mplcoe5  22379  mplbas2  22381  evlslem4  22415  psrbagev1  22416  evlslem2  22418  evlsvvvallem  22430  evlsvvvallem2  22431  evlsvvval  22432  mhmcompl  22460  selvcllem4  22477  selvvvval  22481  mhpvscacl  22505  psdmplcl  22513  evls1fpws  22717  evl1maprhm  22727  mamures  22742  cpmadumatpolylem2  23230  neiptopuni  23478  neiptoptop  23479  restopn2  23525  rncmp  23744  cmpfi  23756  conncn  23774  llyidm  23837  nllyidm  23838  toplly  23839  kgentopon  23887  kgencn2  23906  ptcld  23962  qtopuni  24051  supnfcls  24369  utopbas  24584  metustfbas  24906  rrxcph  25743  rrxmval  25756  rrxdstprj1  25760  evthicc2  25811  volcn  25957  dvres3  26263  dvres3a  26264  dvidlem  26265  dvmptresicc  26266  dvcnp2  26270  dvnadd  26279  dvnres  26281  dvaddbr  26288  dvmulbr  26289  dvcmul  26294  dvcmulf  26295  dvcobr  26296  dvcjbr  26299  dvrec  26305  dveflem  26329  dvef  26330  dvlipcn  26344  dvgt0lem2  26353  lhop1lem  26363  ftc1cn  26393  ftc2  26394  itgpowd  26400  deg1mul3le  26465  coeeulem  26573  dgrcolem1  26622  dgrcolem2  26623  plycpn  26640  rnplynfin  26660  dvntaylp  26728  pserdv  26786  pige3ALT  26878  cxpcn2  27104  rlimcnp3  27325  lgamgulmlem2  27387  basellem2  27439  pntrsumo1  27922  pntrsumbnd  27923  nosupbnd1lem1  28095  noinfbnd1lem1  28110  cutlt  28348  nbupgr  29955  nbumgrvtx  29957  nbgr2vtx1edg  29961  cusgrexilem2  30053  ifpsnprss  30233  1pthon2ve  30785  suppovss  33345  offinsupp1  33388  xrsmulgzz  33640  gsummpt2co  33679  gsummptrev  33687  gsummptp1  33688  gsumfs2d  33692  gsumpart  33694  gsumhashmul  33698  gsummulsubdishift1  33699  symgcom2  33715  pmtrcnelor  33722  tocycfvres1  33741  tocycfvres2  33742  cycpmconjvlem  33772  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnsubrunlem1  33878  fracf1  33939  idomsubr  33941  fldgenid  33951  lindfpropd  34007  lsmsnpridl  34021  qusrn  34030  elrspunidl  34048  mxidlprm  34065  ssmxidl  34069  selvply1rhmlemb  34221  evlextv  34244  mplvrpmrhm  34249  vieta  34282  srapwov  34291  rlmdim  34312  tngdim  34315  matdim  34317  ply1degltdimlem  34324  fedgmullem1  34331  fldextrspunlsplem  34375  algextdeglem8  34426  constrmon  34446  mdetpmtr1  34525  zarclssn  34575  zart0  34581  zarcmplem  34583  pnfneige0  34653  pwsiga  34832  baselcarsg  35008  boolesineq  35157  efmul2picn  35295  reprfz1  35323  breprexplemc  35331  circlemeth  35339  circlevma  35341  circlemethhgt  35342  hgt750lemb  35355  hgt750lema  35356  hgt750leme  35357  tgoldbachgtde  35359  satfsschain  36296  mrsubff1  36446  mrsub0  36448  mrsubccat  36450  mrsubcn  36451  msubff1  36488  mthmpps  36514  wzel  36764  nmulprop  37117  knoppndvlem6  37561  knoppndv  37578  bj-elpwg  38158  bj-restpw  38204  bj-restb  38206  bj-restuni2  38210  ftc1cnnclem  38801  ftc1cnnc  38802  ftc2nc  38812  areacirclem3  38820  welb  38862  cnresima  38890  rngoidl  39150  1psubclN  41193  cdlemefrs32fva  41649  lcmineqlem9  43279  lcmineqlem12  43282  intlewftc  43303  aks4d1p9  43330  primrootspoweq0  43348  sticksstones11  43398  aks6d1c6lem3  43414  aks6d1c6lem4  43415  aks6d1c6lem5  43419  aks6d1c7lem1  43422  addinvcom  43676  evlselv  43810  rgspnid  44362  oacl2g  44524  omabs2  44526  omcl2  44527  tfsconcatb0  44538  naddgeoa  44588  harval3  44731  cnvtrucl0  44816  brfvrtrcld  44926  clsk3nimkb  45232  k0004ss2  45344  extoimad  45356  mnuprd  45452  dvconstbi  45510  ssinc  46307  ssdec  46308  restopn3  46371  founiiun  46399  choicefi  46419  islptre  46836  fnlimfvre  46889  addccncf2  47091  fsumcncf  47093  cncfperiod  47094  negcncfg  47096  cncfuni  47101  icccncfext  47102  cncficcgt0  47103  fprodcncf  47115  dvcnre  47131  fperdvper  47134  itgsinexplem1  47169  itgcoscmulx  47184  fourierdlem113  47434  smfpimne2  48055  predgclnbgrel  49142  isubgrvtxuhgr  49167  fldhmsubcALTV  49635  elbigolo1  49874  iunlub  50137  iinglb  50138  sepfsepc  50247