Theorem sseqtrrid 4062

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  unissint  4996  resdif  6883  fimacnvOLD  7104  tfrlem5  8436  naddunif  8749  domss2  9202  dffi3  9500  cantnfp1lem3  9749  trcl  9797  tcid  9808  r1ordg  9847  r1sssuc  9852  ackbij1lem15  10302  cfsmolem  10339  fin1a2lem7  10475  wunex2  10807  wuncid  10812  trclfvlb  15057  rtrclreclem2  15108  fsumsplit  15789  o1fsum  15861  fprodsplit  16014  phimullem  16826  vdwlem6  17033  ressinbas  17304  mrcssid  17675  mreexexlem2d  17703  acsfiindd  18623  dirge  18673  symgbasfi  19420  efgredlemf  19783  efgredlemd  19786  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumadd  19965  gsumzsplit  19969  gsumsplit2  19971  dprd2da  20086  dmdprdsplit2lem  20089  dmdprdsplit2  20090  dmdprdsplit  20091  dprdsplit  20092  invrpropd  20444  srhmsubc  20702  issubdrg  20803  lspssid  21006  pjcss  21759  aspssid  21921  psdmul  22193  istopon  22939  sscls  23085  ordtbas  23221  cncls2  23302  tgcmp  23430  cmpfi  23437  1stcfb  23474  1stckgenlem  23582  ptbasfi  23610  ptcnplem  23650  ptuncnv  23836  ptunhmeo  23837  fbasrn  23913  cnflf2  24032  fclscmp  24059  alexsublem  24073  ghmcnp  24144  tsmsgsum  24168  tsmsres  24173  tsmssplit  24181  tsmsxplem1  24182  ustssco  24244  mopnfss  24474  cnmpopc  24974  uniiccdif  25632  uniioombllem3  25639  uniioombllem4  25640  itg2splitlem  25803  itg2split  25804  itgsplit  25891  ellimc2  25932  ellimc3  25934  lhop  26075  itgpowd  26111  plyaddlem1  26272  plymullem1  26273  taylthlem2  26434  taylthlem2OLD  26435  mtest  26465  xrlimcnp  27029  fsumharmonic  27073  chtdif  27219  dchrghm  27318  lgsquadlem2  27443  dchrisumlema  27550  dchrisumlem2  27552  dchrisum0lem1b  27577  dchrisum0lem1  27578  pntrlog2bndlem6  27645  pntlemf  27667  precsexlem6  28254  precsexlem7  28255  sltonold  28301  nbupgruvtxres  29442  umgr2adedgwlk  29978  umgr2adedgwlkon  29979  umgr2adedgspth  29981  ex-res  30473  spanss2  31377  mdsymi  32443  padct  32733  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  fldgenssid  33280  ordtconnlem1  33870  issgon  34087  sssigagen  34109  measiuns  34181  sitgclg  34307  cvmliftlem10  35262  satfsschain  35332  fmlasssuc  35357  satfun  35379  rdgssun  37344  ftc1anclem6  37658  heibor1lem  37769  heibor  37781  divrngcl  37917  isdrngo2  37918  igenss  38022  paddunssN  39765  sspadd1  39772  sspadd2  39773  pclssidN  39852  diassdvaN  41017  dochvalr  41314  lcdvbase  41550  nacsfix  42668  isnumbasgrplem2  43061  rgspnssid  43127  tfsconcatrnss12  43311  trrelsuperrel2dg  43633  fvilbd  43651  relexp0a  43678  wnefimgd  44123  grumnudlem  44254  icccncfext  45808  iblsplit  45887  dirkeritg  46023  dirkercncflem2  46025  fourierdlem81  46108  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem111  46138  fouriercn  46153  hspdifhsp  46537  3f1oss1  46990  dfnbgrss  47724  dfnbgrss2  47731  gsumsplit2f  47903  srhmsubcALTV  48048  fdivmpt  48274  fdivpm  48277  refdivpm  48278  mreclat  48669  elpglem2  48804