Theorem 3sstr4i 3974

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 3961	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	mpbir 230	1 ⊢ 𝐶 ⊆ 𝐷

Syntax hints:   = wceq 1540   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3904  df-ss 3914

This theorem is referenced by:  relopabiv  5756  rncoss  5907  imassrn  6004  rnin  6079  inimass  6087  f1ossf1o  7050  ssoprab2i  7439  omopthlem2  8553  1sdom2dom  9104  rankval4  9716  cardf2  9792  r0weon  9861  dcomex  10296  axdc2lem  10297  fpwwe2lem1  10480  canthwe  10500  recmulnq  10813  npex  10835  axresscn  10997  trclublem  14797  bpoly4  15860  2strop1  17029  odlem1  19231  gexlem1  19272  psrbagsn  21369  bwth  22659  2ndcctbss  22704  uniioombllem4  24848  uniioombllem5  24849  eff1olem  25802  birthdaylem1  26199  nvss  29156  lediri  30100  lejdiri  30102  sshhococi  30109  mayetes3i  30292  disjxpin  31127  imadifxp  31140  sxbrsigalem5  32468  eulerpartlemmf  32555  kur14lem6  33385  cvmlift2lem12  33488  bj-xpcossxp  35458  bj-rrhatsscchat  35505  mblfinlem4  35915  lclkrs2  39801  areaquad  41298  corclrcl  41625  corcltrcl  41657  relopabVD  42831  ovolval5lem3  44518