Theorem sseqtr4d 2101

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
sseqtr4d.1	|- (ph -> A (_ B)
sseqtr4d.2	|- (ph -> C = B)

Assertion

Ref	Expression
sseqtr4d	|- (ph -> A (_ C)

Proof of Theorem sseqtr4d

Step	Hyp	Ref	Expression
1		sseqtr4d.1	. 2 |- (ph -> A (_ B)
2		sseqtr4d.2	. . 3 |- (ph -> C = B)
3	2	eqcomd 1483	. 2 |- (ph -> B = C)
4	1, 3	sseqtrd 2100	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 958   (_ wss 2050

This theorem is referenced by:  fimacnv 3816  oaordi 4186  omordi 4203  omlimcl 4215  oen0 4219  rankxplim3 4724  cflim 4921  sscls 7686  iscnp2 7758  metreslem 7819  blss 7850  metcnplem 7883  metcnp 7884  metcnp3 7893  bcthlem18 8013  ssmd2 10234  superpos 10276  atexcht 10303

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain