Theorem sseqtrd 3286

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 3278	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sseqtrrd  3287  fssdmd  5548  resasplitss  5569  nnaword2  6787  erssxp  6830  phpm  7167  nninfninc  7463  nnnninfeq  7468  ioodisj  10395  subsubm  13790  subsubg  14000  trivsubgd  14003  trivnsgd  14020  subsubrng  14522  subrgugrp  14548  subsubrg  14553  islssmd  14696  lspun  14739  lspssp  14740  lsslsp  14766  tgcl  15165  basgen  15181  bastop1  15184  bastop2  15185  clsss2  15230  topssnei  15263  cnntr  15326  txbasval  15368  neitx  15369  cnmpt1res  15397  cnmpt2res  15398  imasnopn  15400  hmeontr  15414  tgioo  15655  reldvg  15780  dvfvalap  15782  dvbss  15786  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcj  15810  vtxdumgrfival  16539