Theorem sseqtrd 3263

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 3255	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 147	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:  sseqtrrd  3264  fssdmd  5493  resasplitss  5513  nnaword2  6677  erssxp  6720  phpm  7047  nninfninc  7313  nnnninfeq  7318  ioodisj  10218  subsubm  13556  subsubg  13774  trivsubgd  13777  trivnsgd  13794  subsubrng  14218  subrgugrp  14244  subsubrg  14249  islssmd  14363  lspun  14406  lspssp  14407  lsslsp  14433  tgcl  14778  basgen  14794  bastop1  14797  bastop2  14798  clsss2  14843  topssnei  14876  cnntr  14939  txbasval  14981  neitx  14982  cnmpt1res  15010  cnmpt2res  15011  imasnopn  15013  hmeontr  15027  tgioo  15268  reldvg  15393  dvfvalap  15395  dvbss  15399  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcj  15423  vtxdumgrfival  16104