Theorem sseqtrrid 3966

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  unissint  4915  resdif  6795  tfrlem5  8312  naddunif  8622  domss2  9067  dffi3  9337  cantnfp1lem3  9592  trcl  9640  tcid  9649  r1ordg  9693  r1sssuc  9698  ackbij1lem15  10146  cfsmolem  10183  fin1a2lem7  10319  wunex2  10652  wuncid  10657  trclfvlb  14961  rtrclreclem2  15012  fsumsplit  15694  o1fsum  15767  fprodsplit  15922  phimullem  16740  vdwlem6  16948  ressinbas  17206  mrcssid  17574  mreexexlem2d  17602  acsfiindd  18510  dirge  18560  symgbasfi  19345  efgredlemf  19707  efgredlemd  19710  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumadd  19889  gsumzsplit  19893  gsumsplit2  19895  dprd2da  20010  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dmdprdsplit  20015  dprdsplit  20016  invrpropd  20389  rgspnssid  20582  srhmsubc  20648  issubdrg  20748  lspssid  20971  pjcss  21706  aspssid  21867  psdmul  22142  istopon  22887  sscls  23031  ordtbas  23167  cncls2  23248  tgcmp  23376  cmpfi  23383  1stcfb  23420  1stckgenlem  23528  ptbasfi  23556  ptcnplem  23596  ptuncnv  23782  ptunhmeo  23783  fbasrn  23859  cnflf2  23978  fclscmp  24005  alexsublem  24019  ghmcnp  24090  tsmsgsum  24114  tsmsres  24119  tsmssplit  24127  tsmsxplem1  24128  ustssco  24190  mopnfss  24418  cnmpopc  24905  uniiccdif  25555  uniioombllem3  25562  uniioombllem4  25563  itg2splitlem  25725  itg2split  25726  itgsplit  25813  ellimc2  25854  ellimc3  25856  lhop  25993  itgpowd  26027  plyaddlem1  26188  plymullem1  26189  taylthlem2  26351  taylthlem2OLD  26352  mtest  26382  xrlimcnp  26945  fsumharmonic  26989  chtdif  27135  dchrghm  27233  lgsquadlem2  27358  dchrisumlema  27465  dchrisumlem2  27467  dchrisum0lem1b  27492  dchrisum0lem1  27493  pntrlog2bndlem6  27560  pntlemf  27582  precsexlem6  28218  precsexlem7  28219  ltonold  28267  nbupgruvtxres  29490  cyclnumvtx  29883  umgr2adedgwlk  30028  umgr2adedgwlkon  30029  umgr2adedgspth  30031  ex-res  30526  spanss2  31431  mdsymi  32497  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  fldgenssid  33389  vietalem  33738  ordtconnlem1  34084  issgon  34283  sssigagen  34305  measiuns  34377  sitgclg  34502  cvmliftlem10  35492  satfsschain  35562  fmlasssuc  35587  satfun  35609  dfttc3gw  36721  rdgssun  37708  ftc1anclem6  38033  heibor1lem  38144  heibor  38156  divrngcl  38292  isdrngo2  38293  igenss  38397  paddunssN  40268  sspadd1  40275  sspadd2  40276  pclssidN  40355  diassdvaN  41520  dochvalr  41817  lcdvbase  42053  nacsfix  43158  isnumbasgrplem2  43550  tfsconcatrnss12  43795  trrelsuperrel2dg  44116  fvilbd  44134  relexp0a  44161  wnefimgd  44606  grumnudlem  44730  icccncfext  46333  iblsplit  46412  dirkeritg  46548  dirkercncflem2  46550  fourierdlem81  46633  fourierdlem89  46641  fourierdlem91  46643  fourierdlem92  46644  fourierdlem111  46663  fouriercn  46678  hspdifhsp  47062  3f1oss1  47535  dfnbgrss  48340  dfnbgrss2  48347  gsumsplit2f  48668  srhmsubcALTV  48813  fdivmpt  49028  fdivpm  49031  refdivpm  49032  mreclat  49484  elpglem2  50199