Theorem ssidd 3246

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  swrd0g  11234  isum  11939  fsum3ser  11951  fsumcl  11954  iprodap  12134  iprodap0  12136  fprodssdc  12144  fprodcl  12161  fprodclf  12189  ennnfoneleminc  13025  submid  13553  mulgnncl  13717  mulgnn0cl  13718  mulgcl  13719  subgid  13755  ablressid  13915  gsumfzreidx  13917  rngressid  13960  ringressid  14069  mulgass3  14091  subrngid  14208  lss1  14369  rlmfn  14460  rlmvalg  14461  rlmbasg  14462  rlmplusgg  14463  rlm0g  14464  rlmmulrg  14466  rlmscabas  14467  rlmvscag  14468  rlmtopng  14469  rlmdsg  14470  restopn2  14900  negcncf  15322  mulcncf  15325  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  dvexp  15428  dvrecap  15430  dvmptcmulcn  15438  dvmptnegcn  15439  dvmptsubcn  15440  dveflem  15443  dvef  15444  ifpsnprss  16154  bj-charfundcALT  16354  gfsumval  16630