Theorem ssidd 3940

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  funfvima2d  7090  suppofss1d  7991  suppofss2d  7992  fpr1  8090  ralxpmap  8642  fissuni  9054  fsuppmptif  9088  fsuppco2  9092  fsuppcor  9093  mapfienlem1  9094  mapfienlem2  9095  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnflem1  9377  trpredpo  9414  htalem  9585  ackbij2lem4  9929  cflim2  9950  fin23lem15  10021  wunex2  10425  swrd0  14299  rtrclreclem1  14696  summolem3  15354  isum  15359  fsumser  15370  fsumcl  15373  flo1  15494  prodmolem3  15571  iprod  15576  iprodn0  15578  fprodss  15586  fprodcl  15590  fprodclf  15630  rpnnen2lem11  15861  eulerthlem2  16411  mremre  17230  catsubcat  17470  yon11  17898  yon12  17899  yon2  17900  yonpropd  17902  oppcyon  17903  yonffth  17918  submid  18364  mulgnncl  18634  mulgnn0cl  18635  mulgcl  18636  subgid  18672  snsymgefmndeq  18917  symggen  18993  gsumzcl2  19426  gsumzf1o  19428  gsum2dlem1  19486  gsum2dlem2  19487  gsum2d  19488  gsumxp2  19496  dprdfinv  19537  dmdprdsplitlem  19555  dprd2db  19561  dpjidcl  19576  ablfac1eu  19591  ablfaclem2  19604  gsumdixp  19763  primefld  19988  lcomfsupp  20078  lss1  20115  rlmbas  20378  rlmplusg  20379  rlm0  20380  rlmmulr  20382  rlmsca  20383  rlmsca2  20384  rlmvsca  20385  rlmtopn  20386  rlmds  20387  regsumsupp  20739  frlmsslsp  20913  frlmup1  20915  rnasclassa  21009  mplsubglem  21115  mpllsslem  21116  mplsubrglem  21120  mplcoe1  21148  mplcoe5  21151  mplbas2  21153  evlslem4  21194  psrbagev1  21195  psrbagev1OLD  21196  evlslem2  21199  mhpvscacl  21254  mamures  21449  cpmadumatpolylem2  21939  neiptopuni  22189  neiptoptop  22190  restopn2  22236  rncmp  22455  cmpfi  22467  conncn  22485  llyidm  22547  nllyidm  22548  toplly  22549  kgentopon  22597  kgencn2  22616  ptcld  22672  qtopuni  22761  supnfcls  23079  utopbas  23295  metustfbas  23619  rrxcph  24461  rrxmval  24474  rrxdstprj1  24478  evthicc2  24529  volcn  24675  dvres3  24982  dvres3a  24983  dvidlem  24984  dvmptresicc  24985  dvnadd  24998  dvnres  25000  dvaddbr  25007  dvmulbr  25008  dvcmul  25013  dvcmulf  25014  dvcobr  25015  dvcjbr  25018  dvrec  25024  dveflem  25048  dvef  25049  dvlipcn  25063  dvgt0lem2  25072  lhop1lem  25082  ftc1cn  25112  ftc2  25113  itgpowd  25119  deg1mul3le  25186  coeeulem  25290  dgrcolem1  25339  dgrcolem2  25340  plycpn  25354  dvntaylp  25435  pserdv  25493  pige3ALT  25581  cxpcn2  25804  rlimcnp3  26022  lgamgulmlem2  26084  basellem2  26136  pntrsumo1  26618  pntrsumbnd  26619  nbupgr  27614  nbumgrvtx  27616  nbgr2vtx1edg  27620  cusgrexilem2  27712  ifpsnprss  27892  1pthon2ve  28419  suppovss  30919  offinsupp1  30964  xrsmulgzz  31189  gsummpt2co  31210  gsumpart  31217  gsumhashmul  31218  symgcom2  31255  pmtrcnelor  31262  tocycfvres1  31279  tocycfvres2  31280  cycpmconjvlem  31310  lindfpropd  31478  lsmsnpridl  31488  elrspunidl  31508  mxidlprm  31542  ssmxidl  31544  rgmoddim  31595  tngdim  31598  matdim  31600  fedgmullem1  31612  mdetpmtr1  31675  zarclssn  31725  zart0  31731  zarcmplem  31733  pnfneige0  31803  pwsiga  31998  baselcarsg  32173  efmul2picn  32476  reprfz1  32504  breprexplemc  32512  circlemeth  32520  circlevma  32522  circlemethhgt  32523  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  satfsschain  33226  mrsubff1  33376  mrsub0  33378  mrsubccat  33380  mrsubcn  33381  msubff1  33418  mthmpps  33444  wzel  33745  nosupbnd1lem1  33838  noinfbnd1lem1  33853  knoppndvlem6  34624  knoppndv  34641  bj-elpwg  35152  bj-restpw  35190  bj-restb  35192  bj-restuni2  35196  ftc1cnnclem  35775  ftc1cnnc  35776  ftc2nc  35786  areacirclem3  35794  welb  35821  cnresima  35849  rngoidl  36109  1psubclN  37885  cdlemefrs32fva  38341  lcmineqlem9  39973  lcmineqlem12  39976  intlewftc  39997  aks4d1p9  40024  sticksstones11  40040  selvval2lem4  40154  evlsbagval  40198  mhphf  40208  addinvcom  40334  rgspnid  40913  harval3  41041  cnvtrucl0  41121  brfvrtrcld  41231  clsk3nimkb  41539  k0004ss2  41651  extoimad  41664  mnuprd  41783  dvconstbi  41841  ssinc  42526  ssdec  42527  founiiun  42604  choicefi  42629  islptre  43050  fnlimfvre  43105  addccncf2  43307  fsumcncf  43309  cncfperiod  43310  negcncfg  43312  cncfuni  43317  icccncfext  43318  cncficcgt0  43319  fprodcncf  43331  dvcnre  43347  fperdvper  43350  itgsinexplem1  43385  itgcoscmulx  43400  submgmid  45235  rnghmsscmap2  45419  rhmsscmap2  45465  fldhmsubc  45530  fldhmsubcALTV  45548  elbigolo1  45791  sepfsepc  46109