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  5551  resasplitss  5572  nnaword2  6791  erssxp  6834  phpm  7171  nninfninc  7469  nnnninfeq  7474  ioodisj  10412  subsubm  13849  subsubg  14059  trivsubgd  14062  trivnsgd  14079  subsubrng  14631  subrgugrp  14657  subsubrg  14662  islssmd  14805  lspun  14848  lspssp  14849  lsslsp  14875  tgcl  15290  basgen  15306  bastop1  15309  bastop2  15310  clsss2  15355  topssnei  15388  cnntr  15451  txbasval  15493  neitx  15494  cnmpt1res  15522  cnmpt2res  15523  imasnopn  15525  hmeontr  15539  tgioo  15780  reldvg  15905  dvfvalap  15907  dvbss  15911  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcj  15935  vtxdumgrfival  16744