Theorem sseqtrrd 3222

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

Syntax hints:   → wi 4   = wceq 1364   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sseqtrrid  3234  fnfvima  5797  tfrlemiubacc  6388  tfr1onlemubacc  6404  tfrcllemubacc  6417  rdgivallem  6439  nnnninf  7192  nninfwlpoimlemg  7241  dfphi2  12388  ctinf  12647  imasaddfnlemg  12957  imasaddvallemg  12958  subsubm  13115  subsubg  13327  subsubrng  13770  subsubrg  13801  lidlss  14032  toponss  14262  ssntr  14358  iscnp3  14439  cnprcl2k  14442  tgcn  14444  tgcnp  14445  ssidcn  14446  cncnp  14466  txcnp  14507  imasnopn  14535  hmeontr  14549  blssec  14674  blssopn  14721  xmettx  14746  metcnp  14748  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  nnsf  15649  nninfsellemsuc  15656