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  7464  nnnninfeq  7469  ioodisj  10406  subsubm  13843  subsubg  14053  trivsubgd  14056  trivnsgd  14073  subsubrng  14606  subrgugrp  14632  subsubrg  14637  islssmd  14780  lspun  14823  lspssp  14824  lsslsp  14850  tgcl  15256  basgen  15272  bastop1  15275  bastop2  15276  clsss2  15321  topssnei  15354  cnntr  15417  txbasval  15459  neitx  15460  cnmpt1res  15488  cnmpt2res  15489  imasnopn  15491  hmeontr  15505  tgioo  15746  reldvg  15871  dvfvalap  15873  dvbss  15877  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcj  15901  vtxdumgrfival  16705