Theorem sseqtrrid 3974

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  unissint  4932  resdif  6838  tfrlem5  8371  naddunif  8687  domss2  9139  dffi3  9407  cantnfp1lem3  9665  trcl  9713  tcid  9722  r1ordg  9768  r1sssuc  9773  ackbij1lem15  10292  cfsmolem  10329  fin1a2lem7  10465  wunex2  10804  wuncid  10809  trclfvlb  15141  rtrclreclem2  15192  fsumsplit  15887  o1fsum  15960  fprodsplit  16113  phimullem  16936  vdwlem6  17144  ressinbas  17403  mrcssid  17771  mreexexlem2d  17799  acsfiindd  18707  dirge  18757  symgbasfi  19573  efgredlemf  19935  efgredlemd  19938  gsumzres  20103  gsumzcl2  20104  gsumzf1o  20106  gsumadd  20117  gsumzsplit  20121  gsumsplit2  20123  dprd2da  20238  dmdprdsplit2lem  20241  dmdprdsplit2  20242  dmdprdsplit  20243  dprdsplit  20244  invrpropd  20628  rgspnssid  20846  srhmsubc  20912  issubdrg  21017  lspssid  21240  pjcss  22002  aspssid  22165  psdmul  22467  istopon  23210  sscls  23354  ordtbas  23490  cncls2  23571  tgcmp  23699  cmpfi  23706  1stcfb  23743  1stckgenlem  23852  ptbasfi  23880  ptcnplem  23920  ptuncnv  24106  ptunhmeo  24107  fbasrn  24183  cnflf2  24302  fclscmp  24329  alexsublem  24343  ghmcnp  24414  tsmsgsum  24438  tsmsres  24443  tsmssplit  24451  tsmsxplem1  24452  ustssco  24514  mopnfss  24742  cnmpopc  25229  uniiccdif  25879  uniioombllem3  25886  uniioombllem4  25887  itg2splitlem  26049  itg2split  26050  itgsplit  26136  ellimc2  26177  ellimc3  26179  lhop  26316  itgpowd  26350  plyaddlem1  26512  plymullem1  26513  taylthlem2  26683  mtest  26713  xrlimcnp  27278  fsumharmonic  27321  chtdif  27467  dchrghm  27565  lgsquadlem2  27690  dchrisumlema  27797  dchrisumlem2  27799  dchrisum0lem1b  27824  dchrisum0lem1  27825  pntrlog2bndlem6  27892  pntlemf  27914  precsexlem6  28580  precsexlem7  28581  ltonold  28629  nbupgruvtxres  29970  cyclnumvtx  30370  umgr2adedgwlk  30516  umgr2adedgwlkon  30517  umgr2adedgspth  30519  ex-res  31024  spanss2  31929  mdsymi  32995  cycpmco2lem5  33673  cycpmco2lem6  33674  cycpmco2lem7  33675  cycpmco2  33676  fldgenssid  33857  vietalem  34193  ordtconnlem1  34538  issgon  34737  sssigagen  34760  measiuns  34832  sitgclg  34957  cvmliftlem10  36028  satfsschain  36098  fmlasssuc  36123  satfun  36145  dfttc3gw  37281  rdgssun  38269  ftc1anclem6  38584  heibor1lem  38711  heibor  38723  divrngcl  38859  isdrngo2  38860  igenss  38964  paddunssN  40833  sspadd1  40840  sspadd2  40841  pclssidN  40920  diassdvaN  42085  dochvalr  42382  lcdvbase  42618  nacsfix  43676  isnumbasgrplem2  44064  tfsconcatrnss12  44309  trrelsuperrel2dg  44630  fvilbd  44648  relexp0a  44675  wnefimgd  45120  grumnudlem  45228  icccncfext  46841  iblsplit  46920  dirkeritg  47056  dirkercncflem2  47058  fourierdlem81  47141  fourierdlem89  47149  fourierdlem91  47151  fourierdlem92  47152  fourierdlem111  47171  fouriercn  47186  hspdifhsp  47570  3f1oss1  48089  dfnbgrss  48894  dfnbgrss2  48901  gsumsplit2f  49221  srhmsubcALTV  49366  fdivmpt  49596  fdivpm  49599  refdivpm  49600  mreclat  50049  elpglem2  50749