Theorem ssidd 3957

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

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

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 3919

This theorem is used by:  pwidg  4580  funfvima2d  7234  suppofss1d  8205  suppofss2d  8206  fpr1  8305  ralxpmap  8906  fissuni  9327  fsuppssov1  9357  fsuppmptif  9372  fsuppco2  9376  fsuppcor  9377  mapfienlem1  9378  mapfienlem2  9379  cantnfp1lem1  9660  cantnfp1lem3  9662  cantnflem1  9671  htalem  9903  ackbij2lem4  10246  cflim2  10268  fin23lem15  10339  wunex2  10750  swrd0  14730  rtrclreclem1  15132  summolem3  15802  isum  15807  fsumser  15818  fsumcl  15821  flo1  15945  prodmolem3  16024  iprod  16029  iprodn0  16031  fprodss  16039  fprodcl  16043  fprodclf  16083  rpnnen2lem11  16316  eulerthlem2  16877  mremre  17692  catsubcat  17932  yon11  18356  yon12  18357  yon2  18358  yonpropd  18360  oppcyon  18361  yonffth  18376  submgmid  18812  submid  18922  mulgnncl  19216  mulgnn0cl  19217  mulgcl  19218  subgid  19255  snsymgefmndeq  19526  symggen  19601  gsumzcl2  20041  gsumzf1o  20043  gsum2dlem1  20101  gsum2dlem2  20102  gsum2d  20103  gsumxp2  20111  dprdfinv  20152  dmdprdsplitlem  20170  dprd2db  20176  dpjidcl  20191  ablfac1eu  20206  ablfaclem2  20219  gsumdixp  20463  subrngid  20715  rnghmsscmap2  20795  rhmsscmap2  20824  fldhmsubc  20955  primefld  20975  lcomfsupp  21090  lss1  21126  rlmbas  21381  rlmplusg  21382  rlm0  21383  rlmmulr  21385  rlmsca  21386  rlmsca2  21387  rlmvsca  21388  rlmtopn  21389  rlmds  21390  rng2idl1cntr  21512  ssdifidl  21552  regsumsupp  21839  frlmsslsp  22013  frlmup1  22015  rnasclassa  22114  mplsubglem  22217  mpllsslem  22218  mplsubrglem  22222  mplcoe1  22257  mplcoe5  22260  mplbas2  22262  evlslem4  22296  psrbagev1  22297  evlslem2  22299  evlsvvvallem  22311  evlsvvvallem2  22312  evlsvvval  22313  mhmcompl  22341  selvcllem4  22358  selvvvval  22362  mhpvscacl  22386  psdmplcl  22394  evls1fpws  22598  evl1maprhm  22608  mamures  22623  cpmadumatpolylem2  23111  neiptopuni  23359  neiptoptop  23360  restopn2  23406  rncmp  23625  cmpfi  23637  conncn  23655  llyidm  23718  nllyidm  23719  toplly  23720  kgentopon  23768  kgencn2  23787  ptcld  23843  qtopuni  23932  supnfcls  24250  utopbas  24465  metustfbas  24787  rrxcph  25624  rrxmval  25637  rrxdstprj1  25641  evthicc2  25692  volcn  25838  dvres3  26145  dvres3a  26146  dvidlem  26147  dvmptresicc  26148  dvcnp2  26152  dvnadd  26161  dvnres  26163  dvaddbr  26170  dvmulbr  26171  dvcmul  26176  dvcmulf  26177  dvcobr  26178  dvcjbr  26181  dvrec  26187  dveflem  26211  dvef  26212  dvlipcn  26226  dvgt0lem2  26235  lhop1lem  26245  ftc1cn  26275  ftc2  26276  itgpowd  26282  deg1mul3le  26347  coeeulem  26454  dgrcolem1  26503  dgrcolem2  26504  plycpn  26523  dvntaylp  26607  pserdv  26665  pige3ALT  26758  cxpcn2  26984  rlimcnp3  27205  lgamgulmlem2  27267  basellem2  27319  pntrsumo1  27802  pntrsumbnd  27803  nosupbnd1lem1  27945  noinfbnd1lem1  27960  cutlt  28198  nbupgr  29805  nbumgrvtx  29807  nbgr2vtx1edg  29811  cusgrexilem2  29903  ifpsnprss  30083  1pthon2ve  30635  suppovss  33155  offinsupp1  33199  xrsmulgzz  33451  gsummpt2co  33490  gsummptrev  33498  gsummptp1  33499  gsumfs2d  33503  gsumpart  33505  gsumhashmul  33509  gsummulsubdishift1  33510  symgcom2  33526  pmtrcnelor  33533  tocycfvres1  33552  tocycfvres2  33553  cycpmconjvlem  33583  elrgspnlem1  33684  elrgspnlem2  33685  elrgspnsubrunlem1  33689  fracf1  33750  idomsubr  33752  fldgenid  33762  lindfpropd  33817  lsmsnpridl  33831  qusrn  33840  elrspunidl  33858  mxidlprm  33875  ssmxidl  33879  selvply1rhmlemb  34031  evlextv  34054  mplvrpmrhm  34059  vieta  34092  srapwov  34101  rlmdim  34122  tngdim  34125  matdim  34127  ply1degltdimlem  34134  fedgmullem1  34141  fldextrspunlsplem  34185  algextdeglem8  34236  constrmon  34256  mdetpmtr1  34335  zarclssn  34385  zart0  34391  zarcmplem  34393  pnfneige0  34463  pwsiga  34642  baselcarsg  34819  boolesineq  34968  efmul2picn  35106  reprfz1  35134  breprexplemc  35142  circlemeth  35150  circlevma  35152  circlemethhgt  35153  hgt750lemb  35166  hgt750lema  35167  hgt750leme  35168  tgoldbachgtde  35170  satfsschain  35945  mrsubff1  36095  mrsub0  36097  mrsubccat  36099  mrsubcn  36100  msubff1  36137  mthmpps  36163  wzel  36403  nmulprop  36772  knoppndvlem6  37216  knoppndv  37233  bj-elpwg  37798  bj-restpw  37844  bj-restb  37846  bj-restuni2  37850  ftc1cnnclem  38442  ftc1cnnc  38443  ftc2nc  38453  areacirclem3  38461  welb  38488  cnresima  38516  rngoidl  38776  1psubclN  40819  cdlemefrs32fva  41275  lcmineqlem9  42905  lcmineqlem12  42908  intlewftc  42929  aks4d1p9  42956  primrootspoweq0  42974  sticksstones11  43024  aks6d1c6lem3  43040  aks6d1c6lem4  43041  aks6d1c6lem5  43045  aks6d1c7lem1  43048  addinvcom  43309  evlselv  43437  rgspnid  44011  oacl2g  44173  omabs2  44175  omcl2  44176  tfsconcatb0  44187  naddgeoa  44237  harval3  44380  cnvtrucl0  44466  brfvrtrcld  44576  clsk3nimkb  44882  k0004ss2  44994  extoimad  45006  mnuprd  45102  dvconstbi  45160  ssinc  45921  ssdec  45922  restopn3  45985  founiiun  46013  choicefi  46033  islptre  46451  fnlimfvre  46504  addccncf2  46706  fsumcncf  46708  cncfperiod  46709  negcncfg  46711  cncfuni  46716  icccncfext  46717  cncficcgt0  46718  fprodcncf  46730  dvcnre  46746  fperdvper  46749  itgsinexplem1  46784  itgcoscmulx  46799  fourierdlem113  47049  smfpimne2  47670  predgclnbgrel  48757  isubgrvtxuhgr  48782  fldhmsubcALTV  49250  elbigolo1  49489  iunlub  49751  iinglb  49752  sepfsepc  49856