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 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  funfvima2d  7117  suppofss1d  8029  suppofss2d  8030  fpr1  8128  ralxpmap  8693  fissuni  9133  fsuppmptif  9167  fsuppco2  9171  fsuppcor  9172  mapfienlem1  9173  mapfienlem2  9174  cantnfp1lem1  9445  cantnfp1lem3  9447  cantnflem1  9456  htalem  9663  ackbij2lem4  10007  cflim2  10028  fin23lem15  10099  wunex2  10503  swrd0  14380  rtrclreclem1  14777  summolem3  15435  isum  15440  fsumser  15451  fsumcl  15454  flo1  15575  prodmolem3  15652  iprod  15657  iprodn0  15659  fprodss  15667  fprodcl  15671  fprodclf  15711  rpnnen2lem11  15942  eulerthlem2  16492  mremre  17322  catsubcat  17563  yon11  17991  yon12  17992  yon2  17993  yonpropd  17995  oppcyon  17996  yonffth  18011  submid  18458  mulgnncl  18728  mulgnn0cl  18729  mulgcl  18730  subgid  18766  snsymgefmndeq  19011  symggen  19087  gsumzcl2  19520  gsumzf1o  19522  gsum2dlem1  19580  gsum2dlem2  19581  gsum2d  19582  gsumxp2  19590  dprdfinv  19631  dmdprdsplitlem  19649  dprd2db  19655  dpjidcl  19670  ablfac1eu  19685  ablfaclem2  19698  gsumdixp  19857  primefld  20082  lcomfsupp  20172  lss1  20209  rlmbas  20474  rlmplusg  20475  rlm0  20476  rlmmulr  20478  rlmsca  20479  rlmsca2  20480  rlmvsca  20481  rlmtopn  20482  rlmds  20483  regsumsupp  20836  frlmsslsp  21012  frlmup1  21014  rnasclassa  21108  mplsubglem  21214  mpllsslem  21215  mplsubrglem  21219  mplcoe1  21247  mplcoe5  21250  mplbas2  21252  evlslem4  21293  psrbagev1  21294  psrbagev1OLD  21295  evlslem2  21298  mhpvscacl  21353  mamures  21548  cpmadumatpolylem2  22040  neiptopuni  22290  neiptoptop  22291  restopn2  22337  rncmp  22556  cmpfi  22568  conncn  22586  llyidm  22648  nllyidm  22649  toplly  22650  kgentopon  22698  kgencn2  22717  ptcld  22773  qtopuni  22862  supnfcls  23180  utopbas  23396  metustfbas  23722  rrxcph  24565  rrxmval  24578  rrxdstprj1  24582  evthicc2  24633  volcn  24779  dvres3  25086  dvres3a  25087  dvidlem  25088  dvmptresicc  25089  dvnadd  25102  dvnres  25104  dvaddbr  25111  dvmulbr  25112  dvcmul  25117  dvcmulf  25118  dvcobr  25119  dvcjbr  25122  dvrec  25128  dveflem  25152  dvef  25153  dvlipcn  25167  dvgt0lem2  25176  lhop1lem  25186  ftc1cn  25216  ftc2  25217  itgpowd  25223  deg1mul3le  25290  coeeulem  25394  dgrcolem1  25443  dgrcolem2  25444  plycpn  25458  dvntaylp  25539  pserdv  25597  pige3ALT  25685  cxpcn2  25908  rlimcnp3  26126  lgamgulmlem2  26188  basellem2  26240  pntrsumo1  26722  pntrsumbnd  26723  nbupgr  27720  nbumgrvtx  27722  nbgr2vtx1edg  27726  cusgrexilem2  27818  ifpsnprss  27999  1pthon2ve  28527  suppovss  31026  offinsupp1  31071  xrsmulgzz  31296  gsummpt2co  31317  gsumpart  31324  gsumhashmul  31325  symgcom2  31362  pmtrcnelor  31369  tocycfvres1  31386  tocycfvres2  31387  cycpmconjvlem  31417  lindfpropd  31585  lsmsnpridl  31595  elrspunidl  31615  mxidlprm  31649  ssmxidl  31651  rgmoddim  31702  tngdim  31705  matdim  31707  fedgmullem1  31719  mdetpmtr1  31782  zarclssn  31832  zart0  31838  zarcmplem  31840  pnfneige0  31910  pwsiga  32107  baselcarsg  32282  efmul2picn  32585  reprfz1  32613  breprexplemc  32621  circlemeth  32629  circlevma  32631  circlemethhgt  32632  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  tgoldbachgtde  32649  satfsschain  33335  mrsubff1  33485  mrsub0  33487  mrsubccat  33489  mrsubcn  33490  msubff1  33527  mthmpps  33553  wzel  33827  nosupbnd1lem1  33920  noinfbnd1lem1  33935  knoppndvlem6  34706  knoppndv  34723  bj-elpwg  35234  bj-restpw  35272  bj-restb  35274  bj-restuni2  35278  ftc1cnnclem  35857  ftc1cnnc  35858  ftc2nc  35868  areacirclem3  35876  welb  35903  cnresima  35931  rngoidl  36191  1psubclN  37965  cdlemefrs32fva  38421  lcmineqlem9  40052  lcmineqlem12  40055  intlewftc  40076  aks4d1p9  40103  sticksstones11  40119  selvval2lem4  40235  evlsbagval  40282  mhphf  40292  addinvcom  40420  rgspnid  41004  harval3  41152  cnvtrucl0  41239  brfvrtrcld  41349  clsk3nimkb  41657  k0004ss2  41769  extoimad  41782  mnuprd  41901  dvconstbi  41959  ssinc  42644  ssdec  42645  founiiun  42722  choicefi  42747  islptre  43167  fnlimfvre  43222  addccncf2  43424  fsumcncf  43426  cncfperiod  43427  negcncfg  43429  cncfuni  43434  icccncfext  43435  cncficcgt0  43436  fprodcncf  43448  dvcnre  43464  fperdvper  43467  itgsinexplem1  43502  itgcoscmulx  43517  submgmid  45358  rnghmsscmap2  45542  rhmsscmap2  45588  fldhmsubc  45653  fldhmsubcALTV  45671  elbigolo1  45914  sepfsepc  46232