Theorem ssidd 3269

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

Assertion

Ref	Expression
ssidd	|- ( ph -> A C_ A )

Proof of Theorem ssidd

Step	Hyp	Ref	Expression
1		ssid 3268	. 2 |- A C_ A
2	1	a1i 9	1 |- ( ph -> A C_ A )

This proof depends on syntax axioms:   -> wi 4   C_ 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  fdmfifsupp  7301  swrd0g  11453  isum  12176  fsum3ser  12188  fsumcl  12191  iprodap  12371  iprodap0  12373  fprodssdc  12381  fprodcl  12398  fprodclf  12426  ennnfoneleminc  13359  submid  13842  mulgnncl  13998  mulgnn0cl  13999  mulgcl  14000  subgid  14036  ablressid  14228  gzsumreidx  14230  gsumvalfi  14241  gsummptfidmadd  14250  rngressid  14359  ringressid  14476  mulgass3  14499  subrngid  14617  lss1  14807  rlmfn  14898  rlmvalg  14899  rlmbasg  14900  rlmplusgg  14901  rlm0g  14902  rlmmulrg  14904  rlmscabas  14905  rlmvscag  14906  rlmtopng  14907  rlmdsg  14908  rnasclassa  15146  restopn2  15426  negcncf  15848  mulcncf  15851  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvexp  15954  dvrecap  15956  dvmptcmulcn  15964  dvmptnegcn  15965  dvmptsubcn  15966  dveflem  15969  dvef  15970  ifpsnprss  16806  bj-charfundcALT  17057