Theorem ssidd 3261

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3213

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  suppofss1dcl  6466  suppofss2dcl  6467  swrd0g  11360  isum  12079  fsum3ser  12091  fsumcl  12094  iprodap  12274  iprodap0  12276  fprodssdc  12284  fprodcl  12301  fprodclf  12329  ennnfoneleminc  13183  submid  13711  mulgnncl  13875  mulgnn0cl  13876  mulgcl  13877  subgid  13913  ablressid  14073  gsumfzreidx  14075  rngressid  14119  ringressid  14228  mulgass3  14251  subrngid  14369  lss1  14559  rlmfn  14650  rlmvalg  14651  rlmbasg  14652  rlmplusgg  14653  rlm0g  14654  rlmmulrg  14656  rlmscabas  14657  rlmvscag  14658  rlmtopng  14659  rlmdsg  14660  restopn2  15097  negcncf  15519  mulcncf  15522  dvidlemap  15605  dvidrelem  15606  dvidsslem  15607  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  dvexp  15625  dvrecap  15627  dvmptcmulcn  15635  dvmptnegcn  15636  dvmptsubcn  15637  dveflem  15640  dvef  15641  ifpsnprss  16387  bj-charfundcALT  16628  gfsumval  16911