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

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

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 3948

This theorem is referenced by:  unissint  4952  resdif  6849  tfrlem5  8402  naddunif  8713  domss2  9158  dffi3  9453  cantnfp1lem3  9702  trcl  9750  tcid  9761  r1ordg  9800  r1sssuc  9805  ackbij1lem15  10255  cfsmolem  10292  fin1a2lem7  10428  wunex2  10760  wuncid  10765  trclfvlb  15029  rtrclreclem2  15080  fsumsplit  15759  o1fsum  15831  fprodsplit  15984  phimullem  16798  vdwlem6  17006  ressinbas  17268  mrcssid  17631  mreexexlem2d  17659  acsfiindd  18567  dirge  18617  symgbasfi  19364  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  20386  rgspnssid  20582  srhmsubc  20648  issubdrg  20749  lspssid  20951  pjcss  21690  aspssid  21852  psdmul  22118  istopon  22866  sscls  23010  ordtbas  23146  cncls2  23227  tgcmp  23355  cmpfi  23362  1stcfb  23399  1stckgenlem  23507  ptbasfi  23535  ptcnplem  23575  ptuncnv  23761  ptunhmeo  23762  fbasrn  23838  cnflf2  23957  fclscmp  23984  alexsublem  23998  ghmcnp  24069  tsmsgsum  24093  tsmsres  24098  tsmssplit  24106  tsmsxplem1  24107  ustssco  24169  mopnfss  24398  cnmpopc  24891  uniiccdif  25549  uniioombllem3  25556  uniioombllem4  25557  itg2splitlem  25719  itg2split  25720  itgsplit  25807  ellimc2  25848  ellimc3  25850  lhop  25991  itgpowd  26027  plyaddlem1  26188  plymullem1  26189  taylthlem2  26352  taylthlem2OLD  26353  mtest  26383  xrlimcnp  26947  fsumharmonic  26991  chtdif  27137  dchrghm  27236  lgsquadlem2  27361  dchrisumlema  27468  dchrisumlem2  27470  dchrisum0lem1b  27495  dchrisum0lem1  27496  pntrlog2bndlem6  27563  pntlemf  27585  precsexlem6  28172  precsexlem7  28173  sltonold  28219  nbupgruvtxres  29352  cyclnumvtx  29748  umgr2adedgwlk  29893  umgr2adedgwlkon  29894  umgr2adedgspth  29896  ex-res  30388  spanss2  31292  mdsymi  32358  padct  32666  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2lem7  33091  cycpmco2  33092  fldgenssid  33255  ordtconnlem1  33882  issgon  34083  sssigagen  34105  measiuns  34177  sitgclg  34303  cvmliftlem10  35258  satfsschain  35328  fmlasssuc  35353  satfun  35375  rdgssun  37338  ftc1anclem6  37664  heibor1lem  37775  heibor  37787  divrngcl  37923  isdrngo2  37924  igenss  38028  paddunssN  39769  sspadd1  39776  sspadd2  39777  pclssidN  39856  diassdvaN  41021  dochvalr  41318  lcdvbase  41554  nacsfix  42686  isnumbasgrplem2  43079  tfsconcatrnss12  43324  trrelsuperrel2dg  43646  fvilbd  43664  relexp0a  43691  wnefimgd  44136  grumnudlem  44261  icccncfext  45859  iblsplit  45938  dirkeritg  46074  dirkercncflem2  46076  fourierdlem81  46159  fourierdlem89  46167  fourierdlem91  46169  fourierdlem92  46170  fourierdlem111  46189  fouriercn  46204  hspdifhsp  46588  3f1oss1  47045  dfnbgrss  47796  dfnbgrss2  47803  gsumsplit2f  48054  srhmsubcALTV  48199  fdivmpt  48419  fdivpm  48422  refdivpm  48423  mreclat  48854  elpglem2  49239