Theorem sseqtrrid 3978

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  unissint  4922  resdif  6784  tfrlem5  8299  naddunif  8608  domss2  9049  dffi3  9315  cantnfp1lem3  9570  trcl  9618  tcid  9629  r1ordg  9668  r1sssuc  9673  ackbij1lem15  10121  cfsmolem  10158  fin1a2lem7  10294  wunex2  10626  wuncid  10631  trclfvlb  14912  rtrclreclem2  14963  fsumsplit  15645  o1fsum  15717  fprodsplit  15870  phimullem  16687  vdwlem6  16895  ressinbas  17153  mrcssid  17520  mreexexlem2d  17548  acsfiindd  18456  dirge  18506  symgbasfi  19289  efgredlemf  19651  efgredlemd  19654  gsumzres  19819  gsumzcl2  19820  gsumzf1o  19822  gsumadd  19833  gsumzsplit  19837  gsumsplit2  19839  dprd2da  19954  dmdprdsplit2lem  19957  dmdprdsplit2  19958  dmdprdsplit  19959  dprdsplit  19960  invrpropd  20334  rgspnssid  20527  srhmsubc  20593  issubdrg  20693  lspssid  20916  pjcss  21651  aspssid  21813  psdmul  22079  istopon  22825  sscls  22969  ordtbas  23105  cncls2  23186  tgcmp  23314  cmpfi  23321  1stcfb  23358  1stckgenlem  23466  ptbasfi  23494  ptcnplem  23534  ptuncnv  23720  ptunhmeo  23721  fbasrn  23797  cnflf2  23916  fclscmp  23943  alexsublem  23957  ghmcnp  24028  tsmsgsum  24052  tsmsres  24057  tsmssplit  24065  tsmsxplem1  24066  ustssco  24128  mopnfss  24356  cnmpopc  24847  uniiccdif  25504  uniioombllem3  25511  uniioombllem4  25512  itg2splitlem  25674  itg2split  25675  itgsplit  25762  ellimc2  25803  ellimc3  25805  lhop  25946  itgpowd  25982  plyaddlem1  26143  plymullem1  26144  taylthlem2  26307  taylthlem2OLD  26308  mtest  26338  xrlimcnp  26903  fsumharmonic  26947  chtdif  27093  dchrghm  27192  lgsquadlem2  27317  dchrisumlema  27424  dchrisumlem2  27426  dchrisum0lem1b  27451  dchrisum0lem1  27452  pntrlog2bndlem6  27519  pntlemf  27541  precsexlem6  28148  precsexlem7  28149  sltonold  28196  nbupgruvtxres  29383  cyclnumvtx  29776  umgr2adedgwlk  29921  umgr2adedgwlkon  29922  umgr2adedgspth  29924  ex-res  30416  spanss2  31320  mdsymi  32386  padct  32696  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  fldgenssid  33274  ordtconnlem1  33932  issgon  34131  sssigagen  34153  measiuns  34225  sitgclg  34350  cvmliftlem10  35326  satfsschain  35396  fmlasssuc  35421  satfun  35443  rdgssun  37411  ftc1anclem6  37737  heibor1lem  37848  heibor  37860  divrngcl  37996  isdrngo2  37997  igenss  38101  paddunssN  39846  sspadd1  39853  sspadd2  39854  pclssidN  39933  diassdvaN  41098  dochvalr  41395  lcdvbase  41631  nacsfix  42744  isnumbasgrplem2  43136  tfsconcatrnss12  43381  trrelsuperrel2dg  43703  fvilbd  43721  relexp0a  43748  wnefimgd  44193  grumnudlem  44317  icccncfext  45924  iblsplit  46003  dirkeritg  46139  dirkercncflem2  46141  fourierdlem81  46224  fourierdlem89  46232  fourierdlem91  46234  fourierdlem92  46235  fourierdlem111  46254  fouriercn  46269  hspdifhsp  46653  3f1oss1  47105  dfnbgrss  47882  dfnbgrss2  47889  gsumsplit2f  48210  srhmsubcALTV  48355  fdivmpt  48571  fdivpm  48574  refdivpm  48575  mreclat  49027  elpglem2  49743