Theorem ssidd 3245

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

Assertion

Ref	Expression
ssidd	⊢ (𝜑 → 𝐴 ⊆ 𝐴)

Proof of Theorem ssidd

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

Syntax hints:   → wi 4   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  swrd0g  11200  isum  11904  fsum3ser  11916  fsumcl  11919  iprodap  12099  iprodap0  12101  fprodssdc  12109  fprodcl  12126  fprodclf  12154  ennnfoneleminc  12990  submid  13518  mulgnncl  13682  mulgnn0cl  13683  mulgcl  13684  subgid  13720  ablressid  13880  gsumfzreidx  13882  rngressid  13925  ringressid  14034  mulgass3  14056  subrngid  14173  lss1  14334  rlmfn  14425  rlmvalg  14426  rlmbasg  14427  rlmplusgg  14428  rlm0g  14429  rlmmulrg  14431  rlmscabas  14432  rlmvscag  14433  rlmtopng  14434  rlmdsg  14435  restopn2  14865  negcncf  15287  mulcncf  15290  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvexp  15393  dvrecap  15395  dvmptcmulcn  15403  dvmptnegcn  15404  dvmptsubcn  15405  dveflem  15408  dvef  15409  ifpsnprss  16064  bj-charfundcALT  16196