Theorem ssidd 3215

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3167

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  swrd0g  11121  isum  11740  fsum3ser  11752  fsumcl  11755  iprodap  11935  iprodap0  11937  fprodssdc  11945  fprodcl  11962  fprodclf  11990  ennnfoneleminc  12826  submid  13353  mulgnncl  13517  mulgnn0cl  13518  mulgcl  13519  subgid  13555  ablressid  13715  gsumfzreidx  13717  rngressid  13760  ringressid  13869  mulgass3  13891  subrngid  14007  lss1  14168  rlmfn  14259  rlmvalg  14260  rlmbasg  14261  rlmplusgg  14262  rlm0g  14263  rlmmulrg  14265  rlmscabas  14266  rlmvscag  14267  rlmtopng  14268  rlmdsg  14269  restopn2  14699  negcncf  15121  mulcncf  15124  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  dvexp  15227  dvrecap  15229  dvmptcmulcn  15237  dvmptnegcn  15238  dvmptsubcn  15239  dveflem  15242  dvef  15243  bj-charfundcALT  15819