Theorem 3sstr4i 3793

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	⊢ 𝐴 ⊆ 𝐵
3sstr4.2	⊢ 𝐶 = 𝐴
3sstr4.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4i	⊢ 𝐶 ⊆ 𝐷

Proof of Theorem 3sstr4i

Step	Hyp	Ref	Expression
1		3sstr4.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		3sstr4.2	. . 3 ⊢ 𝐶 = 𝐴
3		3sstr4.3	. . 3 ⊢ 𝐷 = 𝐵
4	2, 3	sseq12i 3780	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 221	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1631   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737

This theorem is referenced by:  rncoss  5524  imassrn  5618  rnin  5683  inimass  5690  f1ossf1o  6538  ssoprab2i  6896  omopthlem2  7890  rankval4  8894  cardf2  8969  r0weon  9035  dcomex  9471  axdc2lem  9472  fpwwe2lem1  9655  canthwe  9675  recmulnq  9988  npex  10010  axresscn  10171  trclublem  13944  bpoly4  14996  2strop1  16196  odlem1  18161  gexlem1  18201  psrbagsn  19710  bwth  21434  2ndcctbss  21479  uniioombllem4  23574  uniioombllem5  23575  eff1olem  24515  birthdaylem1  24899  nvss  27788  lediri  28736  lejdiri  28738  sshhococi  28745  mayetes3i  28928  disjxpin  29739  imadifxp  29752  sxbrsigalem5  30690  eulerpartlemmf  30777  kur14lem6  31531  cvmlift2lem12  31634  bj-rrhatsscchat  33460  mblfinlem4  33782  lclkrs2  37350  areaquad  38328  corclrcl  38525  corcltrcl  38557  relopabVD  39659