Theorem ssidd 3205

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  isum  11567  fsum3ser  11579  fsumcl  11582  iprodap  11762  iprodap0  11764  fprodssdc  11772  fprodcl  11789  fprodclf  11817  ennnfoneleminc  12653  submid  13179  mulgnncl  13343  mulgnn0cl  13344  mulgcl  13345  subgid  13381  ablressid  13541  gsumfzreidx  13543  rngressid  13586  ringressid  13695  mulgass3  13717  subrngid  13833  lss1  13994  rlmfn  14085  rlmvalg  14086  rlmbasg  14087  rlmplusgg  14088  rlm0g  14089  rlmmulrg  14091  rlmscabas  14092  rlmvscag  14093  rlmtopng  14094  rlmdsg  14095  restopn2  14503  negcncf  14925  mulcncf  14928  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvexp  15031  dvrecap  15033  dvmptcmulcn  15041  dvmptnegcn  15042  dvmptsubcn  15043  dveflem  15046  dvef  15047  bj-charfundcALT  15539