Theorem 3sstr4i 3644

Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4.1	|- A C_ B
3sstr4.2	|- C = A
3sstr4.3	|- D = B

Assertion

Ref	Expression
3sstr4i	|- C C_ D

Proof of Theorem 3sstr4i

Step	Hyp	Ref	Expression
1		3sstr4.1	. 2 |- A C_ B
2		3sstr4.2	. . 3 |- C = A
3		3sstr4.3	. . 3 |- D = B
4	2, 3	sseq12i 3631	. 2 |- ( C C_ D <-> A C_ B )
5	1, 4	mpbir 221	1 |- C C_ D

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  rncoss  5386  imassrn  5477  rnin  5542  inimass  5549  ssoprab2i  6749  omopthlem2  7736  rankval4  8730  cardf2  8769  r0weon  8835  dcomex  9269  axdc2lem  9270  fpwwe2lem1  9453  canthwe  9473  recmulnq  9786  npex  9808  axresscn  9969  trclublem  13734  bpoly4  14790  2strop1  15988  odlem1  17954  gexlem1  17994  psrbagsn  19495  bwth  21213  2ndcctbss  21258  uniioombllem4  23354  uniioombllem5  23355  eff1olem  24294  birthdaylem1  24678  nvss  27448  lediri  28396  lejdiri  28398  sshhococi  28405  mayetes3i  28588  disjxpin  29401  imadifxp  29414  sxbrsigalem5  30350  eulerpartlemmf  30437  kur14lem6  31193  cvmlift2lem12  31296  bj-rrhatsscchat  33123  mblfinlem4  33449  lclkrs2  36829  areaquad  37802  corclrcl  37999  corcltrcl  38031  relopabVD  39137