Theorem eqsstrrd 4034

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrrd.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2740	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 4033	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  ssxpb  6195  fnsnr  7184  suppssof1  8222  oaword1  8588  omword2  8610  oeeui  8638  nnaword1  8665  naddword1  8727  naddunif  8729  cantnfle  9708  cantnflem1d  9725  r1val1  9823  rankr1id  9899  rankxplim3  9918  ackbij2  10279  ttukeylem7  10552  gruima  10839  hashdmpropge2  14518  rlimi  15545  rlimi2  15546  lo1bdd  15552  o1bdd  15563  rlimuni  15582  rlimcld2  15610  o1co  15618  rlimcn1  15620  rlimcn3  15622  o1add2  15656  o1mul2  15657  o1sub2  15658  lo1add  15659  lo1mul  15660  o1dif  15662  rlimneg  15679  rlimsqzlem  15681  lo1le  15684  rlimno1  15686  ramub1lem1  17059  imasaddfnlem  17574  imasvscafn  17583  mrcidb  17659  mrieqv2d  17683  mreexexlem4d  17691  funcres  17946  funcsetcres2  18146  acsfiindd  18610  tsrdir  18661  resmgmhm2  18737  resmhm2  18846  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  f1omvdco2  19480  sylow2a  19651  sylow3lem6  19664  dprdspan  20061  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  dprdsplit  20082  dpjcntz  20086  ablfac1eu  20107  ringidss  20290  subrg1  20598  subrgdvds  20602  subrguss  20603  subrginv  20604  drngdomn  20765  subdrgint  20820  primefld  20822  islss3  20974  lspsnneg  21021  lspextmo  21072  lspsnvs  21133  lsmcv  21160  islbs3  21174  rhmqusnsg  21312  f1lindf  21859  psrbaglesupp  21959  resspsrbas  22011  resspsradd  22012  resspsrmul  22013  evlseu  22124  epttop  23031  neitr  23203  ordtbas  23215  ordtrest2  23227  pnfnei  23243  mnfnei  23244  ordtrestixx  23245  dnsconst  23401  cmpcld  23425  txindis  23657  txtube  23663  xkohaus  23676  xkopt  23678  xkococnlem  23682  xkoinjcn  23710  qtopval2  23719  ssufl  23941  ufldom  23985  cnextcn  24090  tmdgsum2  24119  clssubg  24132  clsnsg  24133  ustund  24245  ustneism  24247  trust  24253  fmucnd  24316  imasdsf1olem  24398  setsmstopn  24505  metequiv2  24538  metust  24586  restmetu  24598  tngtopn  24686  xlebnum  25010  pi1xfrcnv  25103  limcdif  25925  limccnp  25940  limccnp2  25941  limcco  25942  dvn2bss  25980  cpnord  25985  dvcmulf  25996  dvmptres2  26014  dvmptcmul  26016  dvmptntr  26023  dvcnvrelem2  26071  dvcnvre  26072  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  psercnlem2  26482  rlimcxp  27031  o1cxp  27032  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetainflem4  27799  negsbday  28103  sspg  30756  ssps  30758  sspn  30764  mdslj1i  32347  mdslj2i  32348  sh1dle  32379  shatomistici  32389  sumdmdii  32443  unidifsnel  32560  fisuppov1  32697  resf1o  32747  gsumpart  33042  gsumhashmul  33046  symgcom2  33086  submarchi  33175  nsgmgc  33419  lmhmqusker  33424  rhmquskerlem  33432  idlinsubrg  33438  ply1degltdimlem  33649  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  extdg1id  33690  madjusmdetlem1  33787  txomap  33794  rspectopn  33827  zarclssn  33833  zarcmplem  33841  cnvordtrestixx  33873  dya2iocucvr  34265  carsggect  34299  bnj1241  34799  bnj906  34922  fineqvac  35089  cvmscld  35257  fvline2  36127  cldregopn  36313  pibt2  37399  poimirlem15  37621  sstotbnd2  37760  totbndbnd  37775  heibor1  37796  heiborlem8  37804  lsmsat  38989  lssats  38993  lkrpssN  39144  dia2dimlem5  41050  cdlemn2a  41178  dihglblem6  41322  dochocsp  41361  dochdmj1  41372  dochsatshpb  41434  lcfl9a  41487  lclkrlem2r  41506  lclkrlem2s  41507  lclkrlem2v  41510  lcfrlem6  41529  lcfrlem25  41549  lcfrlem35  41559  mapdval2N  41612  mapdin  41644  baerlem5alem2  41693  baerlem5blem2  41694  evlsvvval  42549  evlsbagval  42552  evlsmhpvvval  42581  mhphf  42583  dnnumch2  43033  oege1  43295  omabs2  43321  nadd2rabex  43375  clrellem  43611  iunrelexpmin1  43697  iunrelexpmin2  43701  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  mnuprdlem1  44267  mnuprdlem2  44268  mullimc  45571  islptre  45574  mullimcf  45578  limcmptdm  45590  dvresntr  45873  itgperiod  45936  fourierdlem89  46150  fourierdlem91  46152  iccpartgt  47351  clnbgrgrim  47839  setrecsres  48932