Theorem sseqtrrid 3983

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  unissint  4942  resdif  6849  tfrlem5  8375  naddunif  8689  domss2  9134  dffi3  9401  cantnfp1lem3  9659  trcl  9707  tcid  9716  r1ordg  9760  r1sssuc  9765  ackbij1lem15  10235  cfsmolem  10272  fin1a2lem7  10408  wunex2  10741  wuncid  10746  trclfvlb  15071  rtrclreclem2  15122  fsumsplit  15818  o1fsum  15891  fprodsplit  16046  phimullem  16863  vdwlem6  17071  ressinbas  17330  mrcssid  17698  mreexexlem2d  17726  acsfiindd  18634  dirge  18684  symgbasfi  19480  efgredlemf  19842  efgredlemd  19845  gsumzres  20010  gsumzcl2  20011  gsumzf1o  20013  gsumadd  20024  gsumzsplit  20028  gsumsplit2  20030  dprd2da  20145  dmdprdsplit2lem  20148  dmdprdsplit2  20149  dmdprdsplit  20150  dprdsplit  20151  invrpropd  20533  rgspnssid  20750  srhmsubc  20816  issubdrg  20920  lspssid  21143  pjcss  21903  aspssid  22064  psdmul  22366  istopon  23106  sscls  23250  ordtbas  23386  cncls2  23467  tgcmp  23595  cmpfi  23602  1stcfb  23639  1stckgenlem  23747  ptbasfi  23775  ptcnplem  23815  ptuncnv  24001  ptunhmeo  24002  fbasrn  24078  cnflf2  24197  fclscmp  24224  alexsublem  24238  ghmcnp  24309  tsmsgsum  24333  tsmsres  24338  tsmssplit  24346  tsmsxplem1  24347  ustssco  24409  mopnfss  24637  cnmpopc  25124  uniiccdif  25774  uniioombllem3  25781  uniioombllem4  25782  itg2splitlem  25944  itg2split  25945  itgsplit  26032  ellimc2  26073  ellimc3  26075  lhop  26212  itgpowd  26246  plyaddlem1  26407  plymullem1  26408  taylthlem2  26574  mtest  26604  xrlimcnp  27170  fsumharmonic  27213  chtdif  27359  dchrghm  27457  lgsquadlem2  27582  dchrisumlema  27689  dchrisumlem2  27691  dchrisum0lem1b  27716  dchrisum0lem1  27717  pntrlog2bndlem6  27784  pntlemf  27806  precsexlem6  28442  precsexlem7  28443  ltonold  28491  nbupgruvtxres  29794  cyclnumvtx  30186  umgr2adedgwlk  30331  umgr2adedgwlkon  30332  umgr2adedgspth  30334  ex-res  30829  spanss2  31734  mdsymi  32800  cycpmco2lem5  33481  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmco2  33484  fldgenssid  33665  vietalem  34000  ordtconnlem1  34345  issgon  34544  sssigagen  34567  measiuns  34639  sitgclg  34764  cvmliftlem10  35807  satfsschain  35877  fmlasssuc  35902  satfun  35924  dfttc3gw  37075  rdgssun  38065  ftc1anclem6  38390  heibor1lem  38501  heibor  38513  divrngcl  38649  isdrngo2  38650  igenss  38754  paddunssN  40623  sspadd1  40630  sspadd2  40631  pclssidN  40710  diassdvaN  41875  dochvalr  42172  lcdvbase  42408  nacsfix  43484  isnumbasgrplem2  43872  tfsconcatrnss12  44117  trrelsuperrel2dg  44438  fvilbd  44456  relexp0a  44483  wnefimgd  44928  grumnudlem  45036  icccncfext  46642  iblsplit  46721  dirkeritg  46857  dirkercncflem2  46859  fourierdlem81  46942  fourierdlem89  46950  fourierdlem91  46952  fourierdlem92  46953  fourierdlem111  46972  fouriercn  46987  hspdifhsp  47371  3f1oss1  47853  dfnbgrss  48658  dfnbgrss2  48665  gsumsplit2f  48986  srhmsubcALTV  49131  fdivmpt  49361  fdivpm  49364  refdivpm  49365  mreclat  49816  elpglem2  50531