Theorem sseqtrrid 4049

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 2741	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 4048	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  unissint  4977  resdif  6870  tfrlem5  8419  naddunif  8730  domss2  9175  dffi3  9469  cantnfp1lem3  9718  trcl  9766  tcid  9777  r1ordg  9816  r1sssuc  9821  ackbij1lem15  10271  cfsmolem  10308  fin1a2lem7  10444  wunex2  10776  wuncid  10781  trclfvlb  15044  rtrclreclem2  15095  fsumsplit  15774  o1fsum  15846  fprodsplit  15999  phimullem  16813  vdwlem6  17020  ressinbas  17291  mrcssid  17662  mreexexlem2d  17690  acsfiindd  18611  dirge  18661  symgbasfi  19411  efgredlemf  19774  efgredlemd  19777  gsumzres  19942  gsumzcl2  19943  gsumzf1o  19945  gsumadd  19956  gsumzsplit  19960  gsumsplit2  19962  dprd2da  20077  dmdprdsplit2lem  20080  dmdprdsplit2  20081  dmdprdsplit  20082  dprdsplit  20083  invrpropd  20435  rgspnssid  20631  srhmsubc  20697  issubdrg  20798  lspssid  21001  pjcss  21754  aspssid  21916  psdmul  22188  istopon  22934  sscls  23080  ordtbas  23216  cncls2  23297  tgcmp  23425  cmpfi  23432  1stcfb  23469  1stckgenlem  23577  ptbasfi  23605  ptcnplem  23645  ptuncnv  23831  ptunhmeo  23832  fbasrn  23908  cnflf2  24027  fclscmp  24054  alexsublem  24068  ghmcnp  24139  tsmsgsum  24163  tsmsres  24168  tsmssplit  24176  tsmsxplem1  24177  ustssco  24239  mopnfss  24469  cnmpopc  24969  uniiccdif  25627  uniioombllem3  25634  uniioombllem4  25635  itg2splitlem  25798  itg2split  25799  itgsplit  25886  ellimc2  25927  ellimc3  25929  lhop  26070  itgpowd  26106  plyaddlem1  26267  plymullem1  26268  taylthlem2  26431  taylthlem2OLD  26432  mtest  26462  xrlimcnp  27026  fsumharmonic  27070  chtdif  27216  dchrghm  27315  lgsquadlem2  27440  dchrisumlema  27547  dchrisumlem2  27549  dchrisum0lem1b  27574  dchrisum0lem1  27575  pntrlog2bndlem6  27642  pntlemf  27664  precsexlem6  28251  precsexlem7  28252  sltonold  28298  nbupgruvtxres  29439  umgr2adedgwlk  29975  umgr2adedgwlkon  29976  umgr2adedgspth  29978  ex-res  30470  spanss2  31374  mdsymi  32440  padct  32737  cycpmco2lem5  33133  cycpmco2lem6  33134  cycpmco2lem7  33135  cycpmco2  33136  fldgenssid  33295  ordtconnlem1  33885  issgon  34104  sssigagen  34126  measiuns  34198  sitgclg  34324  cvmliftlem10  35279  satfsschain  35349  fmlasssuc  35374  satfun  35396  rdgssun  37361  ftc1anclem6  37685  heibor1lem  37796  heibor  37808  divrngcl  37944  isdrngo2  37945  igenss  38049  paddunssN  39791  sspadd1  39798  sspadd2  39799  pclssidN  39878  diassdvaN  41043  dochvalr  41340  lcdvbase  41576  nacsfix  42700  isnumbasgrplem2  43093  tfsconcatrnss12  43339  trrelsuperrel2dg  43661  fvilbd  43679  relexp0a  43706  wnefimgd  44151  grumnudlem  44281  icccncfext  45843  iblsplit  45922  dirkeritg  46058  dirkercncflem2  46060  fourierdlem81  46143  fourierdlem89  46151  fourierdlem91  46153  fourierdlem92  46154  fourierdlem111  46173  fouriercn  46188  hspdifhsp  46572  3f1oss1  47025  dfnbgrss  47776  dfnbgrss2  47783  gsumsplit2f  48024  srhmsubcALTV  48169  fdivmpt  48390  fdivpm  48393  refdivpm  48394  mreclat  48786  elpglem2  48943