Theorem ssidd 3269

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  suppofss1dcl  6498  suppofss2dcl  6499  swrd0g  11415  isum  12135  fsum3ser  12147  fsumcl  12150  iprodap  12330  iprodap0  12332  fprodssdc  12340  fprodcl  12357  fprodclf  12385  ennnfoneleminc  13285  submid  13767  mulgnncl  13923  mulgnn0cl  13924  mulgcl  13925  subgid  13961  ablressid  14122  gzsumreidx  14124  gsumvalfi  14135  gsummptfidmadd  14144  rngressid  14236  ringressid  14351  mulgass3  14374  subrngid  14492  lss1  14682  rlmfn  14773  rlmvalg  14774  rlmbasg  14775  rlmplusgg  14776  rlm0g  14777  rlmmulrg  14779  rlmscabas  14780  rlmvscag  14781  rlmtopng  14782  rlmdsg  14783  rnasclassa  15021  restopn2  15267  negcncf  15689  mulcncf  15692  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  dvexp  15795  dvrecap  15797  dvmptcmulcn  15805  dvmptnegcn  15806  dvmptsubcn  15807  dveflem  15810  dvef  15811  ifpsnprss  16567  bj-charfundcALT  16818