Theorem sseqtrrid 4007

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

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

Assertion

Ref	Expression
sseqtrrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrrid

Step	Hyp	Ref	Expression
1		sseqtrrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
2		sseqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3	2	eqcomd 2742	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 4006	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  unissint  4953  resdif  6844  tfrlem5  8399  naddunif  8710  domss2  9155  dffi3  9448  cantnfp1lem3  9699  trcl  9747  tcid  9758  r1ordg  9797  r1sssuc  9802  ackbij1lem15  10252  cfsmolem  10289  fin1a2lem7  10425  wunex2  10757  wuncid  10762  trclfvlb  15032  rtrclreclem2  15083  fsumsplit  15762  o1fsum  15834  fprodsplit  15987  phimullem  16803  vdwlem6  17011  ressinbas  17271  mrcssid  17634  mreexexlem2d  17662  acsfiindd  18568  dirge  18618  symgbasfi  19365  efgredlemf  19727  efgredlemd  19730  gsumzres  19895  gsumzcl2  19896  gsumzf1o  19898  gsumadd  19909  gsumzsplit  19913  gsumsplit2  19915  dprd2da  20030  dmdprdsplit2lem  20033  dmdprdsplit2  20034  dmdprdsplit  20035  dprdsplit  20036  invrpropd  20383  rgspnssid  20579  srhmsubc  20645  issubdrg  20745  lspssid  20947  pjcss  21681  aspssid  21843  psdmul  22109  istopon  22855  sscls  22999  ordtbas  23135  cncls2  23216  tgcmp  23344  cmpfi  23351  1stcfb  23388  1stckgenlem  23496  ptbasfi  23524  ptcnplem  23564  ptuncnv  23750  ptunhmeo  23751  fbasrn  23827  cnflf2  23946  fclscmp  23973  alexsublem  23987  ghmcnp  24058  tsmsgsum  24082  tsmsres  24087  tsmssplit  24095  tsmsxplem1  24096  ustssco  24158  mopnfss  24387  cnmpopc  24878  uniiccdif  25536  uniioombllem3  25543  uniioombllem4  25544  itg2splitlem  25706  itg2split  25707  itgsplit  25794  ellimc2  25835  ellimc3  25837  lhop  25978  itgpowd  26014  plyaddlem1  26175  plymullem1  26176  taylthlem2  26339  taylthlem2OLD  26340  mtest  26370  xrlimcnp  26935  fsumharmonic  26979  chtdif  27125  dchrghm  27224  lgsquadlem2  27349  dchrisumlema  27456  dchrisumlem2  27458  dchrisum0lem1b  27483  dchrisum0lem1  27484  pntrlog2bndlem6  27551  pntlemf  27573  precsexlem6  28171  precsexlem7  28172  sltonold  28219  nbupgruvtxres  29391  cyclnumvtx  29787  umgr2adedgwlk  29932  umgr2adedgwlkon  29933  umgr2adedgspth  29935  ex-res  30427  spanss2  31331  mdsymi  32397  padct  32702  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2lem7  33148  cycpmco2  33149  fldgenssid  33312  ordtconnlem1  33960  issgon  34159  sssigagen  34181  measiuns  34253  sitgclg  34379  cvmliftlem10  35321  satfsschain  35391  fmlasssuc  35416  satfun  35438  rdgssun  37401  ftc1anclem6  37727  heibor1lem  37838  heibor  37850  divrngcl  37986  isdrngo2  37987  igenss  38091  paddunssN  39832  sspadd1  39839  sspadd2  39840  pclssidN  39919  diassdvaN  41084  dochvalr  41381  lcdvbase  41617  nacsfix  42710  isnumbasgrplem2  43103  tfsconcatrnss12  43348  trrelsuperrel2dg  43670  fvilbd  43688  relexp0a  43715  wnefimgd  44160  grumnudlem  44284  icccncfext  45896  iblsplit  45975  dirkeritg  46111  dirkercncflem2  46113  fourierdlem81  46196  fourierdlem89  46204  fourierdlem91  46206  fourierdlem92  46207  fourierdlem111  46226  fouriercn  46241  hspdifhsp  46625  3f1oss1  47084  dfnbgrss  47845  dfnbgrss2  47852  gsumsplit2f  48135  srhmsubcALTV  48280  fdivmpt  48500  fdivpm  48503  refdivpm  48504  mreclat  48951  elpglem2  49556