Theorem ssidd 3245

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  swrd0g  11213  isum  11917  fsum3ser  11929  fsumcl  11932  iprodap  12112  iprodap0  12114  fprodssdc  12122  fprodcl  12139  fprodclf  12167  ennnfoneleminc  13003  submid  13531  mulgnncl  13695  mulgnn0cl  13696  mulgcl  13697  subgid  13733  ablressid  13893  gsumfzreidx  13895  rngressid  13938  ringressid  14047  mulgass3  14069  subrngid  14186  lss1  14347  rlmfn  14438  rlmvalg  14439  rlmbasg  14440  rlmplusgg  14441  rlm0g  14442  rlmmulrg  14444  rlmscabas  14445  rlmvscag  14446  rlmtopng  14447  rlmdsg  14448  restopn2  14878  negcncf  15300  mulcncf  15303  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvexp  15406  dvrecap  15408  dvmptcmulcn  15416  dvmptnegcn  15417  dvmptsubcn  15418  dveflem  15421  dvef  15422  ifpsnprss  16115  bj-charfundcALT  16281