Theorem ssidd 3949

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  funfvima2d  7105  suppofss1d  8011  suppofss2d  8012  fpr1  8110  ralxpmap  8667  fissuni  9102  fsuppmptif  9136  fsuppco2  9140  fsuppcor  9141  mapfienlem1  9142  mapfienlem2  9143  cantnfp1lem1  9414  cantnfp1lem3  9416  cantnflem1  9425  trpredpo  9483  htalem  9655  ackbij2lem4  9999  cflim2  10020  fin23lem15  10091  wunex2  10495  swrd0  14369  rtrclreclem1  14766  summolem3  15424  isum  15429  fsumser  15440  fsumcl  15443  flo1  15564  prodmolem3  15641  iprod  15646  iprodn0  15648  fprodss  15656  fprodcl  15660  fprodclf  15700  rpnnen2lem11  15931  eulerthlem2  16481  mremre  17311  catsubcat  17552  yon11  17980  yon12  17981  yon2  17982  yonpropd  17984  oppcyon  17985  yonffth  18000  submid  18447  mulgnncl  18717  mulgnn0cl  18718  mulgcl  18719  subgid  18755  snsymgefmndeq  19000  symggen  19076  gsumzcl2  19509  gsumzf1o  19511  gsum2dlem1  19569  gsum2dlem2  19570  gsum2d  19571  gsumxp2  19579  dprdfinv  19620  dmdprdsplitlem  19638  dprd2db  19644  dpjidcl  19659  ablfac1eu  19674  ablfaclem2  19687  gsumdixp  19846  primefld  20071  lcomfsupp  20161  lss1  20198  rlmbas  20463  rlmplusg  20464  rlm0  20465  rlmmulr  20467  rlmsca  20468  rlmsca2  20469  rlmvsca  20470  rlmtopn  20471  rlmds  20472  regsumsupp  20825  frlmsslsp  21001  frlmup1  21003  rnasclassa  21097  mplsubglem  21203  mpllsslem  21204  mplsubrglem  21208  mplcoe1  21236  mplcoe5  21239  mplbas2  21241  evlslem4  21282  psrbagev1  21283  psrbagev1OLD  21284  evlslem2  21287  mhpvscacl  21342  mamures  21537  cpmadumatpolylem2  22029  neiptopuni  22279  neiptoptop  22280  restopn2  22326  rncmp  22545  cmpfi  22557  conncn  22575  llyidm  22637  nllyidm  22638  toplly  22639  kgentopon  22687  kgencn2  22706  ptcld  22762  qtopuni  22851  supnfcls  23169  utopbas  23385  metustfbas  23711  rrxcph  24554  rrxmval  24567  rrxdstprj1  24571  evthicc2  24622  volcn  24768  dvres3  25075  dvres3a  25076  dvidlem  25077  dvmptresicc  25078  dvnadd  25091  dvnres  25093  dvaddbr  25100  dvmulbr  25101  dvcmul  25106  dvcmulf  25107  dvcobr  25108  dvcjbr  25111  dvrec  25117  dveflem  25141  dvef  25142  dvlipcn  25156  dvgt0lem2  25165  lhop1lem  25175  ftc1cn  25205  ftc2  25206  itgpowd  25212  deg1mul3le  25279  coeeulem  25383  dgrcolem1  25432  dgrcolem2  25433  plycpn  25447  dvntaylp  25528  pserdv  25586  pige3ALT  25674  cxpcn2  25897  rlimcnp3  26115  lgamgulmlem2  26177  basellem2  26229  pntrsumo1  26711  pntrsumbnd  26712  nbupgr  27709  nbumgrvtx  27711  nbgr2vtx1edg  27715  cusgrexilem2  27807  ifpsnprss  27987  1pthon2ve  28514  suppovss  31013  offinsupp1  31058  xrsmulgzz  31283  gsummpt2co  31304  gsumpart  31311  gsumhashmul  31312  symgcom2  31349  pmtrcnelor  31356  tocycfvres1  31373  tocycfvres2  31374  cycpmconjvlem  31404  lindfpropd  31572  lsmsnpridl  31582  elrspunidl  31602  mxidlprm  31636  ssmxidl  31638  rgmoddim  31689  tngdim  31692  matdim  31694  fedgmullem1  31706  mdetpmtr1  31769  zarclssn  31819  zart0  31825  zarcmplem  31827  pnfneige0  31897  pwsiga  32094  baselcarsg  32269  efmul2picn  32572  reprfz1  32600  breprexplemc  32608  circlemeth  32616  circlevma  32618  circlemethhgt  32619  hgt750lemb  32632  hgt750lema  32633  hgt750leme  32634  tgoldbachgtde  32636  satfsschain  33322  mrsubff1  33472  mrsub0  33474  mrsubccat  33476  mrsubcn  33477  msubff1  33514  mthmpps  33540  wzel  33814  nosupbnd1lem1  33907  noinfbnd1lem1  33922  knoppndvlem6  34693  knoppndv  34710  bj-elpwg  35221  bj-restpw  35259  bj-restb  35261  bj-restuni2  35265  ftc1cnnclem  35844  ftc1cnnc  35845  ftc2nc  35855  areacirclem3  35863  welb  35890  cnresima  35918  rngoidl  36178  1psubclN  37954  cdlemefrs32fva  38410  lcmineqlem9  40042  lcmineqlem12  40045  intlewftc  40066  aks4d1p9  40093  sticksstones11  40109  selvval2lem4  40225  evlsbagval  40272  mhphf  40282  addinvcom  40410  rgspnid  40994  harval3  41122  cnvtrucl0  41202  brfvrtrcld  41312  clsk3nimkb  41620  k0004ss2  41732  extoimad  41745  mnuprd  41864  dvconstbi  41922  ssinc  42607  ssdec  42608  founiiun  42685  choicefi  42710  islptre  43131  fnlimfvre  43186  addccncf2  43388  fsumcncf  43390  cncfperiod  43391  negcncfg  43393  cncfuni  43398  icccncfext  43399  cncficcgt0  43400  fprodcncf  43412  dvcnre  43428  fperdvper  43431  itgsinexplem1  43466  itgcoscmulx  43481  submgmid  45316  rnghmsscmap2  45500  rhmsscmap2  45546  fldhmsubc  45611  fldhmsubcALTV  45629  elbigolo1  45872  sepfsepc  46190