Theorem sseqtrrid 3951

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  unissint  4931  resdif  6846  tfrlem5  8390  naddunif  8706  domss2  9158  dffi3  9426  cantnfp1lem3  9684  trcl  9732  tcid  9741  r1ordg  9788  r1sssuc  9793  ackbij1lem15  10314  cfsmolem  10351  fin1a2lem7  10487  wunex2  10826  wuncid  10831  trclfvlb  15166  rtrclreclem2  15217  fsumsplit  15912  o1fsum  15985  fprodsplit  16138  phimullem  16961  vdwlem6  17169  ressinbas  17428  mrcssid  17796  mreexexlem2d  17824  acsfiindd  18732  dirge  18782  symgbasfi  19598  efgredlemf  19960  efgredlemd  19963  gsumzres  20128  gsumzcl2  20129  gsumzf1o  20131  gsumadd  20142  gsumzsplit  20146  gsumsplit2  20148  dprd2da  20263  dmdprdsplit2lem  20266  dmdprdsplit2  20267  dmdprdsplit  20268  dprdsplit  20269  invrpropd  20653  rgspnssid  20871  srhmsubc  20937  issubdrg  21042  lspssid  21265  pjcss  22027  aspssid  22190  psdmul  22492  istopon  23235  sscls  23379  ordtbas  23515  cncls2  23596  tgcmp  23724  cmpfi  23731  1stcfb  23768  1stckgenlem  23877  ptbasfi  23905  ptcnplem  23945  ptuncnv  24131  ptunhmeo  24132  fbasrn  24208  cnflf2  24327  fclscmp  24354  alexsublem  24368  ghmcnp  24439  tsmsgsum  24463  tsmsres  24468  tsmssplit  24476  tsmsxplem1  24477  ustssco  24539  mopnfss  24767  cnmpopc  25254  uniiccdif  25904  uniioombllem3  25911  uniioombllem4  25912  itg2splitlem  26074  itg2split  26075  itgsplit  26161  ellimc2  26202  ellimc3  26204  lhop  26341  itgpowd  26375  plyaddlem1  26537  plymullem1  26538  taylthlem2  26706  mtest  26736  xrlimcnp  27301  fsumharmonic  27344  chtdif  27490  dchrghm  27588  lgsquadlem2  27713  dchrisumlema  27820  dchrisumlem2  27822  dchrisum0lem1b  27847  dchrisum0lem1  27848  pntrlog2bndlem6  27915  pntlemf  27937  precsexlem6  28603  precsexlem7  28604  ltonold  28652  nbupgruvtxres  29993  cyclnumvtx  30393  umgr2adedgwlk  30539  umgr2adedgwlkon  30540  umgr2adedgspth  30542  ex-res  31047  spanss2  31952  mdsymi  33018  cycpmco2lem5  33737  cycpmco2lem6  33738  cycpmco2lem7  33739  cycpmco2  33740  fldgenssid  33921  vietalem  34257  ordtconnlem1  34602  issgon  34801  sssigagen  34824  measiuns  34896  sitgclg  35020  cvmliftlem10  36145  satfsschain  36215  fmlasssuc  36240  satfun  36262  dfttc3gw  37403  rdgssun  38394  ftc1anclem6  38709  heibor1lem  38836  heibor  38848  divrngcl  38984  isdrngo2  38985  igenss  39089  paddunssN  40958  sspadd1  40965  sspadd2  40966  pclssidN  41045  diassdvaN  42210  dochvalr  42507  lcdvbase  42743  nacsfix  43816  isnumbasgrplem2  44199  tfsconcatrnss12  44444  trrelsuperrel2dg  44764  fvilbd  44782  relexp0a  44809  wnefimgd  45254  grumnudlem  45362  icccncfext  46990  iblsplit  47069  dirkeritg  47205  dirkercncflem2  47207  fourierdlem81  47290  fourierdlem89  47298  fourierdlem91  47300  fourierdlem92  47301  fourierdlem111  47320  fouriercn  47335  hspdifhsp  47719  3f1oss1  48238  dfnbgrss  49043  dfnbgrss2  49050  gsumsplit2f  49370  srhmsubcALTV  49515  fdivmpt  49745  fdivpm  49748  refdivpm  49749  mreclat  50204  elpglem2  50973