Theorem ssidd 3225

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  swrd0g  11158  isum  11862  fsum3ser  11874  fsumcl  11877  iprodap  12057  iprodap0  12059  fprodssdc  12067  fprodcl  12084  fprodclf  12112  ennnfoneleminc  12948  submid  13476  mulgnncl  13640  mulgnn0cl  13641  mulgcl  13642  subgid  13678  ablressid  13838  gsumfzreidx  13840  rngressid  13883  ringressid  13992  mulgass3  14014  subrngid  14130  lss1  14291  rlmfn  14382  rlmvalg  14383  rlmbasg  14384  rlmplusgg  14385  rlm0g  14386  rlmmulrg  14388  rlmscabas  14389  rlmvscag  14390  rlmtopng  14391  rlmdsg  14392  restopn2  14822  negcncf  15244  mulcncf  15247  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  dvexp  15350  dvrecap  15352  dvmptcmulcn  15360  dvmptnegcn  15361  dvmptsubcn  15362  dveflem  15365  dvef  15366  bj-charfundcALT  16082