Theorem sseqtrrd 3234

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2212	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3233	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  sseqtrrid  3246  fnfvima  5829  tfrlemiubacc  6426  tfr1onlemubacc  6442  tfrcllemubacc  6455  rdgivallem  6477  nnnninf  7240  nninfwlpoimlemg  7289  ccatass  11078  swrdval2  11118  dfphi2  12592  ctinf  12851  imasaddfnlemg  13196  imasaddvallemg  13197  subsubm  13365  subsubg  13583  subsubrng  14026  subsubrg  14057  lidlss  14288  toponss  14548  ssntr  14644  iscnp3  14725  cnprcl2k  14728  tgcn  14730  tgcnp  14731  ssidcn  14732  cncnp  14752  txcnp  14793  imasnopn  14821  hmeontr  14835  blssec  14960  blssopn  15007  xmettx  15032  metcnp  15034  plyaddlem1  15269  plymullem1  15270  plycoeid3  15279  nnsf  16057  nninfsellemsuc  16064