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  6504  suppofss2dcl  6505  swrd0g  11434  isum  12154  fsum3ser  12166  fsumcl  12169  iprodap  12349  iprodap0  12351  fprodssdc  12359  fprodcl  12376  fprodclf  12404  ennnfoneleminc  13304  submid  13786  mulgnncl  13942  mulgnn0cl  13943  mulgcl  13944  subgid  13980  ablressid  14141  gzsumreidx  14143  gsumvalfi  14154  gsummptfidmadd  14163  rngressid  14255  ringressid  14370  mulgass3  14393  subrngid  14511  lss1  14701  rlmfn  14792  rlmvalg  14793  rlmbasg  14794  rlmplusgg  14795  rlm0g  14796  rlmmulrg  14798  rlmscabas  14799  rlmvscag  14800  rlmtopng  14801  rlmdsg  14802  rnasclassa  15040  restopn2  15286  negcncf  15708  mulcncf  15711  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  dvexp  15814  dvrecap  15816  dvmptcmulcn  15824  dvmptnegcn  15825  dvmptsubcn  15826  dveflem  15829  dvef  15830  ifpsnprss  16596  bj-charfundcALT  16847