Theorem sseqtrd 2097

Description: Substitution of equality into a subclass relationship.

Hypotheses

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

Assertion

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

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 |- (ph -> A (_ B)
2		sseqtrd.2	. . 3 |- (ph -> B = C)
3	2	sseq2d 2089	. 2 |- (ph -> (A (_ B <-> A (_ C))
4	1, 3	mpbid 195	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 956   (_ wss 2047

This theorem is referenced by:  sseqtr4d 2098  fconst4 3851  nnaword2 4245  unifiOLD 4557  r1val1 4658  rankr1id 4697  fodom 4798  tgclt 7624  tgss2t 7637  2basgent 7641  bastop2 7643  clsss2 7703  iscncl 7770  cnconst 7780  dnsconst 7788  unirnbl 7875  metelcls 7965  shsub2t 9289  ococint 9297  spanssoc 9319  shub2t 9353  chub2t 9431  spanpr 9503  ssmd1 10238  mdslj1 10246  mdslj2 10247  mdslmd3 10259  mdexch 10262  irredlem1 10317  atcvat3 10323  atcvat4 10324  mdsymlem1 10330  mdsymlem5 10334

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain