Theorem sseqtrrd 3264

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 2235	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3263	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sseqtrrid  3276  fnfvima  5884  tfrlemiubacc  6491  tfr1onlemubacc  6507  tfrcllemubacc  6520  rdgivallem  6542  nnnninf  7319  nninfwlpoimlemg  7368  ccatass  11178  swrdval2  11225  dfphi2  12785  ctinf  13044  imasaddfnlemg  13390  imasaddvallemg  13391  subsubm  13559  subsubg  13777  subsubrng  14221  subsubrg  14252  lidlss  14483  toponss  14743  ssntr  14839  iscnp3  14920  cnprcl2k  14923  tgcn  14925  tgcnp  14926  ssidcn  14927  cncnp  14947  txcnp  14988  imasnopn  15016  hmeontr  15030  blssec  15155  blssopn  15202  xmettx  15227  metcnp  15229  plyaddlem1  15464  plymullem1  15465  plycoeid3  15474  nnsf  16557  nninfsellemsuc  16564