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 ⊢ (𝜑 → 𝐴 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220

This proof depends on 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 proof 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 used by:  suppofss1dcl  6508  suppofss2dcl  6509  swrd0g  11455  isum  12178  fsum3ser  12190  fsumcl  12193  iprodap  12373  iprodap0  12375  fprodssdc  12383  fprodcl  12400  fprodclf  12428  ennnfoneleminc  13361  submid  13844  mulgnncl  14000  mulgnn0cl  14001  mulgcl  14002  subgid  14038  ablressid  14230  gzsumreidx  14232  gsumvalfi  14243  gsummptfidmadd  14252  rngressid  14361  ringressid  14478  mulgass3  14501  subrngid  14619  lss1  14809  rlmfn  14900  rlmvalg  14901  rlmbasg  14902  rlmplusgg  14903  rlm0g  14904  rlmmulrg  14906  rlmscabas  14907  rlmvscag  14908  rlmtopng  14909  rlmdsg  14910  rnasclassa  15148  restopn2  15421  negcncf  15843  mulcncf  15846  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  dvexp  15949  dvrecap  15951  dvmptcmulcn  15959  dvmptnegcn  15960  dvmptsubcn  15961  dveflem  15964  dvef  15965  ifpsnprss  16801  bj-charfundcALT  17052