Theorem sseqtrrid 3977

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

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

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 2734

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

This theorem is used by:  unissint  4935  resdif  6843  tfrlem5  8372  naddunif  8686  domss2  9138  dffi3  9405  cantnfp1lem3  9663  trcl  9711  tcid  9720  r1ordg  9764  r1sssuc  9769  ackbij1lem15  10239  cfsmolem  10276  fin1a2lem7  10412  wunex2  10751  wuncid  10756  trclfvlb  15085  rtrclreclem2  15136  fsumsplit  15831  o1fsum  15904  fprodsplit  16059  phimullem  16876  vdwlem6  17084  ressinbas  17343  mrcssid  17711  mreexexlem2d  17739  acsfiindd  18647  dirge  18697  symgbasfi  19512  efgredlemf  19874  efgredlemd  19877  gsumzres  20042  gsumzcl2  20043  gsumzf1o  20045  gsumadd  20056  gsumzsplit  20060  gsumsplit2  20062  dprd2da  20177  dmdprdsplit2lem  20180  dmdprdsplit2  20181  dmdprdsplit  20182  dprdsplit  20183  invrpropd  20565  rgspnssid  20782  srhmsubc  20848  issubdrg  20952  lspssid  21175  pjcss  21935  aspssid  22098  psdmul  22400  istopon  23143  sscls  23287  ordtbas  23423  cncls2  23504  tgcmp  23632  cmpfi  23639  1stcfb  23676  1stckgenlem  23785  ptbasfi  23813  ptcnplem  23853  ptuncnv  24039  ptunhmeo  24040  fbasrn  24116  cnflf2  24235  fclscmp  24262  alexsublem  24276  ghmcnp  24347  tsmsgsum  24371  tsmsres  24376  tsmssplit  24384  tsmsxplem1  24385  ustssco  24447  mopnfss  24675  cnmpopc  25162  uniiccdif  25812  uniioombllem3  25819  uniioombllem4  25820  itg2splitlem  25982  itg2split  25983  itgsplit  26070  ellimc2  26111  ellimc3  26113  lhop  26250  itgpowd  26284  plyaddlem1  26446  plymullem1  26447  taylthlem2  26617  mtest  26647  xrlimcnp  27213  fsumharmonic  27256  chtdif  27402  dchrghm  27500  lgsquadlem2  27625  dchrisumlema  27732  dchrisumlem2  27734  dchrisum0lem1b  27759  dchrisum0lem1  27760  pntrlog2bndlem6  27827  pntlemf  27849  precsexlem6  28485  precsexlem7  28486  ltonold  28534  nbupgruvtxres  29875  cyclnumvtx  30275  umgr2adedgwlk  30421  umgr2adedgwlkon  30422  umgr2adedgspth  30424  ex-res  30929  spanss2  31834  mdsymi  32900  cycpmco2lem5  33578  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmco2  33581  fldgenssid  33762  vietalem  34097  ordtconnlem1  34442  issgon  34641  sssigagen  34664  measiuns  34736  sitgclg  34861  cvmliftlem10  35881  satfsschain  35951  fmlasssuc  35976  satfun  35998  dfttc3gw  37150  rdgssun  38140  ftc1anclem6  38455  heibor1lem  38567  heibor  38579  divrngcl  38715  isdrngo2  38716  igenss  38820  paddunssN  40689  sspadd1  40696  sspadd2  40697  pclssidN  40776  diassdvaN  41941  dochvalr  42238  lcdvbase  42474  nacsfix  43565  isnumbasgrplem2  43953  tfsconcatrnss12  44198  trrelsuperrel2dg  44519  fvilbd  44537  relexp0a  44564  wnefimgd  45009  grumnudlem  45117  icccncfext  46723  iblsplit  46802  dirkeritg  46938  dirkercncflem2  46940  fourierdlem81  47023  fourierdlem89  47031  fourierdlem91  47033  fourierdlem92  47034  fourierdlem111  47053  fouriercn  47068  hspdifhsp  47452  3f1oss1  47971  dfnbgrss  48776  dfnbgrss2  48783  gsumsplit2f  49103  srhmsubcALTV  49248  fdivmpt  49478  fdivpm  49481  refdivpm  49482  mreclat  49931  elpglem2  50646