Theorem sseqtrrid 4009

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3950

This theorem is referenced by:  unissint  4954  resdif  6850  tfrlem5  8403  naddunif  8714  domss2  9159  dffi3  9454  cantnfp1lem3  9703  trcl  9751  tcid  9762  r1ordg  9801  r1sssuc  9806  ackbij1lem15  10256  cfsmolem  10293  fin1a2lem7  10429  wunex2  10761  wuncid  10766  trclfvlb  15030  rtrclreclem2  15081  fsumsplit  15760  o1fsum  15832  fprodsplit  15985  phimullem  16799  vdwlem6  17007  ressinbas  17272  mrcssid  17636  mreexexlem2d  17664  acsfiindd  18572  dirge  18622  symgbasfi  19369  efgredlemf  19732  efgredlemd  19735  gsumzres  19900  gsumzcl2  19901  gsumzf1o  19903  gsumadd  19914  gsumzsplit  19918  gsumsplit2  19920  dprd2da  20035  dmdprdsplit2lem  20038  dmdprdsplit2  20039  dmdprdsplit  20040  dprdsplit  20041  invrpropd  20391  rgspnssid  20587  srhmsubc  20653  issubdrg  20754  lspssid  20956  pjcss  21703  aspssid  21865  psdmul  22137  istopon  22885  sscls  23029  ordtbas  23165  cncls2  23246  tgcmp  23374  cmpfi  23381  1stcfb  23418  1stckgenlem  23526  ptbasfi  23554  ptcnplem  23594  ptuncnv  23780  ptunhmeo  23781  fbasrn  23857  cnflf2  23976  fclscmp  24003  alexsublem  24017  ghmcnp  24088  tsmsgsum  24112  tsmsres  24117  tsmssplit  24125  tsmsxplem1  24126  ustssco  24188  mopnfss  24417  cnmpopc  24910  uniiccdif  25568  uniioombllem3  25575  uniioombllem4  25576  itg2splitlem  25738  itg2split  25739  itgsplit  25826  ellimc2  25867  ellimc3  25869  lhop  26010  itgpowd  26046  plyaddlem1  26207  plymullem1  26208  taylthlem2  26371  taylthlem2OLD  26372  mtest  26402  xrlimcnp  26966  fsumharmonic  27010  chtdif  27156  dchrghm  27255  lgsquadlem2  27380  dchrisumlema  27487  dchrisumlem2  27489  dchrisum0lem1b  27514  dchrisum0lem1  27515  pntrlog2bndlem6  27582  pntlemf  27604  precsexlem6  28191  precsexlem7  28192  sltonold  28238  nbupgruvtxres  29371  cyclnumvtx  29767  umgr2adedgwlk  29912  umgr2adedgwlkon  29913  umgr2adedgspth  29915  ex-res  30407  spanss2  31311  mdsymi  32377  padct  32678  cycpmco2lem5  33096  cycpmco2lem6  33097  cycpmco2lem7  33098  cycpmco2  33099  fldgenssid  33261  ordtconnlem1  33864  issgon  34065  sssigagen  34087  measiuns  34159  sitgclg  34285  cvmliftlem10  35240  satfsschain  35310  fmlasssuc  35335  satfun  35357  rdgssun  37320  ftc1anclem6  37646  heibor1lem  37757  heibor  37769  divrngcl  37905  isdrngo2  37906  igenss  38010  paddunssN  39751  sspadd1  39758  sspadd2  39759  pclssidN  39838  diassdvaN  41003  dochvalr  41300  lcdvbase  41536  nacsfix  42668  isnumbasgrplem2  43061  tfsconcatrnss12  43307  trrelsuperrel2dg  43629  fvilbd  43647  relexp0a  43674  wnefimgd  44119  grumnudlem  44249  icccncfext  45847  iblsplit  45926  dirkeritg  46062  dirkercncflem2  46064  fourierdlem81  46147  fourierdlem89  46155  fourierdlem91  46157  fourierdlem92  46158  fourierdlem111  46177  fouriercn  46192  hspdifhsp  46576  3f1oss1  47033  dfnbgrss  47784  dfnbgrss2  47791  gsumsplit2f  48042  srhmsubcALTV  48187  fdivmpt  48407  fdivpm  48410  refdivpm  48411  mreclat  48842  elpglem2  49227