Theorem ssidd 3945

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802

This theorem depends on definitions:  df-bi 208  df-ss 3907

This theorem is referenced by:  funfvima2d  7183  suppofss1d  8151  suppofss2d  8152  fpr1  8250  ralxpmap  8841  fissuni  9264  fsuppssov1  9294  fsuppmptif  9309  fsuppco2  9313  fsuppcor  9314  mapfienlem1  9315  mapfienlem2  9316  cantnfp1lem1  9597  cantnfp1lem3  9599  cantnflem1  9608  htalem  9818  ackbij2lem4  10161  cflim2  10183  fin23lem15  10254  wunex2  10659  swrd0  14619  rtrclreclem1  15017  summolem3  15674  isum  15679  fsumser  15690  fsumcl  15693  flo1  15817  prodmolem3  15896  iprod  15901  iprodn0  15903  fprodss  15911  fprodcl  15915  fprodclf  15955  rpnnen2lem11  16189  eulerthlem2  16750  mremre  17564  catsubcat  17804  yon11  18228  yon12  18229  yon2  18230  yonpropd  18232  oppcyon  18233  yonffth  18248  submgmid  18672  submid  18776  mulgnncl  19063  mulgnn0cl  19064  mulgcl  19065  subgid  19102  snsymgefmndeq  19368  symggen  19443  gsumzcl2  19883  gsumzf1o  19885  gsum2dlem1  19943  gsum2dlem2  19944  gsum2d  19945  gsumxp2  19953  dprdfinv  19994  dmdprdsplitlem  20012  dprd2db  20018  dpjidcl  20033  ablfac1eu  20048  ablfaclem2  20061  gsumdixp  20296  subrngid  20528  rnghmsscmap2  20608  rhmsscmap2  20637  fldhmsubc  20764  primefld  20784  lcomfsupp  20899  lss1  20935  rlmbas  21190  rlmplusg  21191  rlm0  21192  rlmmulr  21194  rlmsca  21195  rlmsca2  21196  rlmvsca  21197  rlmtopn  21198  rlmds  21199  rng2idl1cntr  21305  regsumsupp  21604  frlmsslsp  21778  frlmup1  21780  rnasclassa  21877  mplsubglem  21980  mpllsslem  21981  mplsubrglem  21985  mplcoe1  22020  mplcoe5  22023  mplbas2  22025  evlslem4  22059  psrbagev1  22060  evlslem2  22062  evlsvvvallem  22074  evlsvvvallem2  22075  evlsvvval  22076  mhmcompl  22104  selvcllem4  22121  selvvvval  22125  mhpvscacl  22149  psdmplcl  22157  evls1fpws  22362  evl1maprhm  22372  mamures  22387  cpmadumatpolylem2  22872  neiptopuni  23120  neiptoptop  23121  restopn2  23167  rncmp  23386  cmpfi  23398  conncn  23416  llyidm  23478  nllyidm  23479  toplly  23480  kgentopon  23528  kgencn2  23547  ptcld  23603  qtopuni  23692  supnfcls  24010  utopbas  24225  metustfbas  24547  rrxcph  25384  rrxmval  25397  rrxdstprj1  25401  evthicc2  25452  volcn  25598  dvres3  25905  dvres3a  25906  dvidlem  25907  dvmptresicc  25908  dvcnp2  25912  dvnadd  25921  dvnres  25923  dvaddbr  25930  dvmulbr  25931  dvcmul  25936  dvcmulf  25937  dvcobr  25938  dvcjbr  25941  dvrec  25947  dveflem  25971  dvef  25972  dvlipcn  25986  dvgt0lem2  25995  lhop1lem  26005  ftc1cn  26035  ftc2  26036  itgpowd  26042  deg1mul3le  26107  coeeulem  26214  dgrcolem1  26263  dgrcolem2  26264  plycpn  26280  dvntaylp  26361  pserdv  26419  pige3ALT  26509  cxpcn2  26735  rlimcnp3  26956  lgamgulmlem2  27018  basellem2  27070  pntrsumo1  27553  pntrsumbnd  27554  nosupbnd1lem1  27697  noinfbnd1lem1  27712  cutlt  27949  nbupgr  29438  nbumgrvtx  29440  nbgr2vtx1edg  29444  cusgrexilem2  29536  ifpsnprss  29716  1pthon2ve  30249  suppovss  32780  offinsupp1  32825  xrsmulgzz  33095  gsummpt2co  33136  gsummptrev  33144  gsummptp1  33145  gsumfs2d  33149  gsumpart  33151  gsumhashmul  33155  gsummulsubdishift1  33156  symgcom2  33172  pmtrcnelor  33179  tocycfvres1  33198  tocycfvres2  33199  cycpmconjvlem  33229  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnsubrunlem1  33335  fracf1  33398  idomsubr  33400  fldgenid  33410  lindfpropd  33472  lsmsnpridl  33488  qusrn  33499  elrspunidl  33518  ssdifidl  33547  mxidlprm  33560  ssmxidl  33564  selvply1rhmlemb  33710  evlextv  33733  mplvrpmrhm  33738  vieta  33771  srapwov  33780  rlmdim  33801  tngdim  33804  matdim  33806  ply1degltdimlem  33813  fedgmullem1  33820  fldextrspunlsplem  33864  algextdeglem8  33915  constrmon  33935  mdetpmtr1  34014  zarclssn  34064  zart0  34070  zarcmplem  34072  pnfneige0  34142  pwsiga  34321  baselcarsg  34497  boolesineq  34646  efmul2picn  34787  reprfz1  34815  breprexplemc  34823  circlemeth  34831  circlevma  34833  circlemethhgt  34834  hgt750lemb  34847  hgt750lema  34848  hgt750leme  34849  tgoldbachgtde  34851  satfsschain  35593  mrsubff1  35743  mrsub0  35745  mrsubccat  35747  mrsubcn  35748  msubff1  35785  mthmpps  35811  wzel  36051  knoppndvlem6  36824  knoppndv  36841  bj-elpwg  37406  bj-restpw  37451  bj-restb  37453  bj-restuni2  37457  ftc1cnnclem  38059  ftc1cnnc  38060  ftc2nc  38070  areacirclem3  38078  welb  38104  cnresima  38132  rngoidl  38392  1psubclN  40437  cdlemefrs32fva  40893  lcmineqlem9  42523  lcmineqlem12  42526  intlewftc  42547  aks4d1p9  42574  primrootspoweq0  42592  sticksstones11  42642  aks6d1c6lem3  42658  aks6d1c6lem4  42659  aks6d1c6lem5  42663  aks6d1c7lem1  42666  addinvcom  42910  evlselv  43040  rgspnid  43614  oacl2g  43776  omabs2  43778  omcl2  43779  tfsconcatb0  43790  naddgeoa  43840  harval3  43983  cnvtrucl0  44069  brfvrtrcld  44179  clsk3nimkb  44485  k0004ss2  44597  extoimad  44609  mnuprd  44721  dvconstbi  44779  ssinc  45535  ssdec  45536  restopn3  45599  founiiun  45627  choicefi  45647  islptre  46065  fnlimfvre  46118  addccncf2  46320  fsumcncf  46322  cncfperiod  46323  negcncfg  46325  cncfuni  46330  icccncfext  46331  cncficcgt0  46332  fprodcncf  46344  dvcnre  46360  fperdvper  46363  itgsinexplem1  46398  itgcoscmulx  46413  smfpimne2  47284  predgclnbgrel  48331  isubgrvtxuhgr  48356  fldhmsubcALTV  48825  elbigolo1  49049  iunlub  49312  iinglb  49313  sepfsepc  49419