Theorem sseq12d 2080

Description: An equality deduction for the subclass relationship.

Hypotheses

Ref	Expression
sseq1d.1	|- (ph -> A = B)
sseq12d.2	|- (ph -> C = D)

Assertion

Ref	Expression
sseq12d	|- (ph -> (A (_ C <-> B (_ D))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 |- (ph -> A = B)
2	1	sseq1d 2078	. 2 |- (ph -> (A (_ C <-> B (_ C))
3		sseq12d.2	. . 3 |- (ph -> C = D)
4	3	sseq2d 2079	. 2 |- (ph -> (B (_ C <-> B (_ D))
5	2, 4	bitrd 526	1 |- (ph -> (A (_ C <-> B (_ D))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   (_ wss 2037

This theorem is referenced by:  3sstr3d 2093  3sstr4d 2094  tz6.12-2 3724  oawordri 4168  omwordi 4186  omwordri 4187  oewordi 4202  oewordri 4203  oeworde 4204  inf3lem1 4585  alephle 4856  dominf 4876  basis1t 7556  eltgt 7560  bcthlem16 7948  isps 8571  hsupss 9224  shslejt 9265  ledit 9378  osum 9503  pjoi0t 9579  mdbr4 10135  dmdbr4 10142  dmdi4 10143  mdslle1 10152  mdslle2 10153  mdslmd1lem1 10160  mdslmd1lem2 10161  mdslmd1lem3 10162  mdslmd1lem4 10163  mdslmd1 10164  sumdmdlem2 10253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-in 2041  df-ss 2043

Copyright terms: Public domain