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  11447  isum  12170  fsum3ser  12182  fsumcl  12185  iprodap  12365  iprodap0  12367  fprodssdc  12375  fprodcl  12392  fprodclf  12420  ennnfoneleminc  13353  submid  13835  mulgnncl  13991  mulgnn0cl  13992  mulgcl  13993  subgid  14029  ablressid  14190  gzsumreidx  14192  gsumvalfi  14203  gsummptfidmadd  14212  rngressid  14304  ringressid  14419  mulgass3  14442  subrngid  14560  lss1  14750  rlmfn  14841  rlmvalg  14842  rlmbasg  14843  rlmplusgg  14844  rlm0g  14845  rlmmulrg  14847  rlmscabas  14848  rlmvscag  14849  rlmtopng  14850  rlmdsg  14851  rnasclassa  15089  restopn2  15336  negcncf  15758  mulcncf  15761  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvcjbr  15861  dvexp  15864  dvrecap  15866  dvmptcmulcn  15874  dvmptnegcn  15875  dvmptsubcn  15876  dveflem  15879  dvef  15880  ifpsnprss  16706  bj-charfundcALT  16957