Theorem ssidd 3168

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  isum  11348  fsum3ser  11360  fsumcl  11363  iprodap  11543  iprodap0  11545  fprodssdc  11553  fprodcl  11570  fprodclf  11598  ennnfoneleminc  12366  submid  12699  restopn2  12977  negcncf  13382  mulcncf  13385  dvidlemap  13454  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvexp  13469  dvrecap  13471  dvmptcmulcn  13477  dvmptnegcn  13478  dvmptsubcn  13479  dveflem  13481  dvef  13482  bj-charfundcALT  13844