Theorem eqsstrd 2092

Description: Substitution of equality into a subclass relationship.

Hypotheses

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

Assertion

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

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 |- (ph -> B (_ C)
2		eqsstrd.1	. . 3 |- (ph -> A = B)
3	2	sseq1d 2085	. 2 |- (ph -> (A (_ C <-> B (_ C))
4	1, 3	mpbird 196	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 955   (_ wss 2044

This theorem is referenced by:  eqsstr3d 2093  snsspr 2467  fimacnv 3805  oawordeulem 4181  oewordri 4212  oaabslem 4244  mapsspw 4334  fodomr 4472  r1val1 4641  cardonle 4805  carduniima 4873  cfub 4891  cflecard 4895  ioossre 6341  uzssz 6375  infxpidmlem7 7518  infxpidmlem8 7519  subbas2 7605  ntrss2 7650  lpsscls 7705  cnconst 7740  blssm 7812  rnblssm 7813  opnfss 7820  tgioolem 7876  chssoct 9374  specclt 9782  elnlfn2t 9810  mdsl0 10193  mdexch 10218  atcvat3 10279  dmdbr5at 10305  clsrebb 10439  subsp 10488

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-in 2048  df-ss 2050

Copyright terms: Public domain