Theorem sseqtr4 2094

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 1479	. 2 |- B = C
4	1, 3	sseqtr 2093	1 |- A (_ C

Syntax hints:   = wceq 956   (_ wss 2047

This theorem is referenced by:  eqimss2i 2112  iunxdif2 2598  intabs 2733  sssucid 3047  opabssxp 3234  relopab 3266  dmresi 3399  cnvimass 3423  ssrnres 3481  cnvcnv 3486  fvclss 3855  tfrlem11 3921  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  oawordeulem 4188  mapex 4328  mapsspw 4341  trcl 4645  rankpw 4684  aceq3lem 4732  aceq3 4733  brdom7disj 4804  brdom6disj 4805  cfsuc 4915  cfom 4916  ressxr 5498  nnssnn0 6102  ser1f0 7170  opnfss 7858  cncfmet1 7906  remetba 7909  tgioolem 7914  tgioo 7915  ghsubgi 8138  nmcnc 8342  ipasslem8 8497  shsspwh 9118  hhssabl 9132  hhssnv 9134  hhshsslem1 9137  sshhococ 9469  pjoml6 9532  osumlem8 9585  osumcor 9587  mayete3 9673  pjclem1 10123  pjc 10128  mdcompl 10356  dmdcompl 10357  efilcp 10572  efilcpOLD 10573  stoi 10639

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