Theorem sseqtrd 3262

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	sseq2d 3254	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 3203  df-ss 3210

This theorem is referenced by:  sseqtrrd  3263  fssdmd  5487  resasplitss  5507  nnaword2  6668  erssxp  6711  phpm  7035  nninfninc  7301  nnnninfeq  7306  ioodisj  10201  subsubm  13531  subsubg  13749  trivsubgd  13752  trivnsgd  13769  subsubrng  14193  subrgugrp  14219  subsubrg  14224  islssmd  14338  lspun  14381  lspssp  14382  lsslsp  14408  tgcl  14753  basgen  14769  bastop1  14772  bastop2  14773  clsss2  14818  topssnei  14851  cnntr  14914  txbasval  14956  neitx  14957  cnmpt1res  14985  cnmpt2res  14986  imasnopn  14988  hmeontr  15002  tgioo  15243  reldvg  15368  dvfvalap  15370  dvbss  15374  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcj  15398  vtxdumgrfival  16057