Theorem ssidd 3970

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  funfvima2d  7187  suppofss1d  8140  suppofss2d  8141  fpr1  8239  ralxpmap  8841  fissuni  9308  fsuppmptif  9344  fsuppco2  9348  fsuppcor  9349  mapfienlem1  9350  mapfienlem2  9351  cantnfp1lem1  9623  cantnfp1lem3  9625  cantnflem1  9634  htalem  9841  ackbij2lem4  10187  cflim2  10208  fin23lem15  10279  wunex2  10683  swrd0  14558  rtrclreclem1  14954  summolem3  15610  isum  15615  fsumser  15626  fsumcl  15629  flo1  15750  prodmolem3  15827  iprod  15832  iprodn0  15834  fprodss  15842  fprodcl  15846  fprodclf  15886  rpnnen2lem11  16117  eulerthlem2  16665  mremre  17498  catsubcat  17739  yon11  18167  yon12  18168  yon2  18169  yonpropd  18171  oppcyon  18172  yonffth  18187  submid  18635  mulgnncl  18905  mulgnn0cl  18906  mulgcl  18907  subgid  18944  snsymgefmndeq  19190  symggen  19266  gsumzcl2  19701  gsumzf1o  19703  gsum2dlem1  19761  gsum2dlem2  19762  gsum2d  19763  gsumxp2  19771  dprdfinv  19812  dmdprdsplitlem  19830  dprd2db  19836  dpjidcl  19851  ablfac1eu  19866  ablfaclem2  19879  gsumdixp  20047  primefld  20328  lcomfsupp  20419  lss1  20456  rlmbas  20723  rlmplusg  20724  rlm0  20725  rlmmulr  20727  rlmsca  20728  rlmsca2  20729  rlmvsca  20730  rlmtopn  20731  rlmds  20732  regsumsupp  21063  frlmsslsp  21239  frlmup1  21241  rnasclassa  21335  mplsubglem  21442  mpllsslem  21443  mplsubrglem  21447  mplcoe1  21475  mplcoe5  21478  mplbas2  21480  evlslem4  21521  psrbagev1  21522  psrbagev1OLD  21523  evlslem2  21526  mhpvscacl  21581  mamures  21776  cpmadumatpolylem2  22268  neiptopuni  22518  neiptoptop  22519  restopn2  22565  rncmp  22784  cmpfi  22796  conncn  22814  llyidm  22876  nllyidm  22877  toplly  22878  kgentopon  22926  kgencn2  22945  ptcld  23001  qtopuni  23090  supnfcls  23408  utopbas  23624  metustfbas  23950  rrxcph  24793  rrxmval  24806  rrxdstprj1  24810  evthicc2  24861  volcn  25007  dvres3  25314  dvres3a  25315  dvidlem  25316  dvmptresicc  25317  dvnadd  25330  dvnres  25332  dvaddbr  25339  dvmulbr  25340  dvcmul  25345  dvcmulf  25346  dvcobr  25347  dvcjbr  25350  dvrec  25356  dveflem  25380  dvef  25381  dvlipcn  25395  dvgt0lem2  25404  lhop1lem  25414  ftc1cn  25444  ftc2  25445  itgpowd  25451  deg1mul3le  25518  coeeulem  25622  dgrcolem1  25671  dgrcolem2  25672  plycpn  25686  dvntaylp  25767  pserdv  25825  pige3ALT  25913  cxpcn2  26136  rlimcnp3  26354  lgamgulmlem2  26416  basellem2  26468  pntrsumo1  26950  pntrsumbnd  26951  nosupbnd1lem1  27093  noinfbnd1lem1  27108  nbupgr  28355  nbumgrvtx  28357  nbgr2vtx1edg  28361  cusgrexilem2  28453  ifpsnprss  28634  1pthon2ve  29161  suppovss  31665  offinsupp1  31712  xrsmulgzz  31939  gsummpt2co  31960  gsumpart  31967  gsumhashmul  31968  symgcom2  32005  pmtrcnelor  32012  tocycfvres1  32029  tocycfvres2  32030  cycpmconjvlem  32060  fldgenid  32157  lindfpropd  32242  lsmsnpridl  32252  elrspunidl  32279  mxidlprm  32313  ssmxidl  32315  evls1fpws  32348  rgmoddim  32392  tngdim  32395  matdim  32397  ply1degltdimlem  32404  fedgmullem1  32411  mdetpmtr1  32493  zarclssn  32543  zart0  32549  zarcmplem  32551  pnfneige0  32621  pwsiga  32818  baselcarsg  32995  efmul2picn  33298  reprfz1  33326  breprexplemc  33334  circlemeth  33342  circlevma  33344  circlemethhgt  33345  hgt750lemb  33358  hgt750lema  33359  hgt750leme  33360  tgoldbachgtde  33362  satfsschain  34045  mrsubff1  34195  mrsub0  34197  mrsubccat  34199  mrsubcn  34200  msubff1  34237  mthmpps  34263  wzel  34485  knoppndvlem6  35056  knoppndv  35073  bj-elpwg  35596  bj-restpw  35636  bj-restb  35638  bj-restuni2  35642  ftc1cnnclem  36222  ftc1cnnc  36223  ftc2nc  36233  areacirclem3  36241  welb  36268  cnresima  36296  rngoidl  36556  1psubclN  38480  cdlemefrs32fva  38936  lcmineqlem9  40567  lcmineqlem12  40570  intlewftc  40591  aks4d1p9  40618  sticksstones11  40637  mhmcompl  40794  evlsbagval  40806  selvcllem4  40817  mhphf  40829  addinvcom  40958  rgspnid  41557  oacl2g  41723  omabs2  41725  omcl2  41726  tfsconcatb0  41737  naddgeoa  41788  harval3  41932  cnvtrucl0  42018  brfvrtrcld  42128  clsk3nimkb  42434  k0004ss2  42546  extoimad  42559  mnuprd  42678  dvconstbi  42736  ssinc  43419  ssdec  43420  restopn3  43488  founiiun  43518  choicefi  43542  islptre  43980  fnlimfvre  44035  addccncf2  44237  fsumcncf  44239  cncfperiod  44240  negcncfg  44242  cncfuni  44247  icccncfext  44248  cncficcgt0  44249  fprodcncf  44261  dvcnre  44277  fperdvper  44280  itgsinexplem1  44315  itgcoscmulx  44330  smfpimne2  45201  submgmid  46207  rnghmsscmap2  46391  rhmsscmap2  46437  fldhmsubc  46502  fldhmsubcALTV  46520  elbigolo1  46763  sepfsepc  47080