Theorem ssidd 3248

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  swrd0g  11242  isum  11948  fsum3ser  11960  fsumcl  11963  iprodap  12143  iprodap0  12145  fprodssdc  12153  fprodcl  12170  fprodclf  12198  ennnfoneleminc  13034  submid  13562  mulgnncl  13726  mulgnn0cl  13727  mulgcl  13728  subgid  13764  ablressid  13924  gsumfzreidx  13926  rngressid  13970  ringressid  14079  mulgass3  14101  subrngid  14218  lss1  14379  rlmfn  14470  rlmvalg  14471  rlmbasg  14472  rlmplusgg  14473  rlm0g  14474  rlmmulrg  14476  rlmscabas  14477  rlmvscag  14478  rlmtopng  14479  rlmdsg  14480  restopn2  14910  negcncf  15332  mulcncf  15335  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvexp  15438  dvrecap  15440  dvmptcmulcn  15448  dvmptnegcn  15449  dvmptsubcn  15450  dveflem  15453  dvef  15454  ifpsnprss  16197  bj-charfundcALT  16425  gfsumval  16701