Theorem 3sstr4i 3750

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

Syntax hints:   = wceq 1596   ⊆ wss 3680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-in 3687  df-ss 3694

This theorem is referenced by:  rncoss  5493  imassrn  5587  rnin  5652  inimass  5659  ssoprab2i  6866  omopthlem2  7856  rankval4  8843  cardf2  8882  r0weon  8948  dcomex  9382  axdc2lem  9383  fpwwe2lem1  9566  canthwe  9586  recmulnq  9899  npex  9921  axresscn  10082  trclublem  13856  bpoly4  14910  2strop1  16111  odlem1  18075  gexlem1  18115  psrbagsn  19618  bwth  21336  2ndcctbss  21381  uniioombllem4  23475  uniioombllem5  23476  eff1olem  24414  birthdaylem1  24798  nvss  27678  lediri  28626  lejdiri  28628  sshhococi  28635  mayetes3i  28818  disjxpin  29629  imadifxp  29642  sxbrsigalem5  30580  eulerpartlemmf  30667  kur14lem6  31421  cvmlift2lem12  31524  bj-rrhatsscchat  33355  mblfinlem4  33681  lclkrs2  37248  areaquad  38221  corclrcl  38418  corcltrcl  38450  relopabVD  39553