Theorem sseqtr4 2091

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
sseqtr4.1	|- A (_ B
sseqtr4.2	|- C = B

Assertion

Ref	Expression
sseqtr4	|- A (_ C

Proof of Theorem sseqtr4

Step	Hyp	Ref	Expression
1		sseqtr4.1	. 2 |- A (_ B
2		sseqtr4.2	. . 3 |- C = B
3	2	eqcomi 1477	. 2 |- B = C
4	1, 3	sseqtr 2090	1 |- A (_ C

Syntax hints:   = wceq 955   (_ wss 2044

This theorem is referenced by:  eqimss2i 2109  iunxdif2 2594  intabs 2729  sssucid 3043  opabssxp 3230  relopab 3262  dmresi 3395  cnvimass 3419  ssrnres 3477  cnvcnv 3482  fvclss 3850  tfrlem11 3916  tz7.44-1 3923  tz7.44-2 3924  tz7.44-3 3925  oawordeulem 4181  mapex 4321  mapsspw 4334  trcl 4628  rankpw 4667  aceq3lem 4715  aceq3 4716  brdom7disj 4787  brdom6disj 4788  cfsuc 4898  cfom 4899  ressxr 5481  nnssnn0 6059  ser1f0 7123  opnfss 7820  cncfmet1 7868  remetba 7871  tgioolem 7876  tgioo 7877  ghsubgi 8102  nmcnc 8304  ipasslem8 8456  shsspwh 9073  hhssabl 9087  hhssnv 9089  hhshsslem1 9092  sshhococ 9424  pjoml6 9489  osumlem8 9542  osumcor 9544  mayete3 9630  pjclem1 10079  pjc 10084  mdcompl 10312  dmdcompl 10313  efilcp 10504  stoi 10555

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