Theorem sseqtrrd 3209

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  sseqtrrid  3221  fnfvima  5771  tfrlemiubacc  6354  tfr1onlemubacc  6370  tfrcllemubacc  6383  rdgivallem  6405  nnnninf  7153  nninfwlpoimlemg  7202  dfphi2  12251  ctinf  12480  imasaddfnlemg  12788  imasaddvallemg  12789  subsubm  12932  subsubg  13133  subsubrng  13558  subsubrg  13589  lidlss  13789  toponss  13978  ssntr  14074  iscnp3  14155  cnprcl2k  14158  tgcn  14160  tgcnp  14161  ssidcn  14162  cncnp  14182  txcnp  14223  imasnopn  14251  hmeontr  14265  blssec  14390  blssopn  14437  xmettx  14462  metcnp  14464  nnsf  15208  nninfsellemsuc  15215