Theorem eqsstrrd 3986

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ssxpb  6131  fnsnr  7116  suppssof1  8135  oaword1  8504  omword2  8526  oeeui  8554  nnaword1  8581  naddword1  8642  naddunif  8644  cantnfle  9616  cantnflem1d  9633  r1val1  9731  rankr1id  9807  rankxplim3  9826  ackbij2  10188  ttukeylem7  10460  gruima  10747  hashdmpropge2  14394  rlimi  15407  rlimi2  15408  lo1bdd  15414  o1bdd  15425  rlimuni  15444  rlimcld2  15472  o1co  15480  rlimcn1  15482  rlimcn3  15484  o1add2  15518  o1mul2  15519  o1sub2  15520  lo1add  15521  lo1mul  15522  o1dif  15524  rlimneg  15543  rlimsqzlem  15545  lo1le  15548  rlimno1  15550  ramub1lem1  16909  imasaddfnlem  17424  imasvscafn  17433  mrcidb  17509  mrieqv2d  17533  mreexexlem4d  17541  funcres  17796  funcsetcres2  17993  acsfiindd  18456  tsrdir  18507  resmhm2  18646  f1omvdco2  19244  sylow2a  19415  sylow3lem6  19428  dprdspan  19820  dprd2dlem2  19833  dprd2dlem1  19834  dprd2da  19835  dmdprdsplit2lem  19838  dprdsplit  19841  dpjcntz  19845  ablfac1eu  19866  ringidss  20012  subrg1  20280  subrgdvds  20284  subrguss  20285  subrginv  20286  subdrgint  20326  primefld  20328  islss3  20477  lspsnneg  20524  lspextmo  20574  lspsnvs  20634  lsmcv  20661  islbs3  20675  drngdomn  20810  f1lindf  21265  psrbaglesupp  21363  psrbaglesuppOLD  21364  resspsrbas  21421  resspsradd  21422  resspsrmul  21423  evlseu  21530  epttop  22396  neitr  22568  ordtbas  22580  ordtrest2  22592  pnfnei  22608  mnfnei  22609  ordtrestixx  22610  dnsconst  22766  cmpcld  22790  txindis  23022  txtube  23028  xkohaus  23041  xkopt  23043  xkococnlem  23047  xkoinjcn  23075  qtopval2  23084  ssufl  23306  ufldom  23350  cnextcn  23455  tmdgsum2  23484  clssubg  23497  clsnsg  23498  ustund  23610  ustneism  23612  trust  23618  fmucnd  23681  imasdsf1olem  23763  setsmstopn  23870  metequiv2  23903  metust  23951  restmetu  23963  tngtopn  24051  xlebnum  24365  pi1xfrcnv  24457  limcdif  25277  limccnp  25292  limccnp2  25293  limcco  25294  dvn2bss  25331  cpnord  25336  dvcmulf  25346  dvmptres2  25363  dvmptcmul  25365  dvmptntr  25372  dvcnvrelem2  25419  dvcnvre  25420  taylthlem1  25769  taylthlem2  25770  ulmdvlem3  25798  psercnlem2  25820  rlimcxp  26360  o1cxp  26361  nosupbnd2lem1  27100  noinfbnd2lem1  27115  noetainflem4  27125  sspg  29733  ssps  29735  sspn  29741  mdslj1i  31324  mdslj2i  31325  sh1dle  31356  shatomistici  31366  sumdmdii  31420  unidifsnel  31526  resf1o  31715  gsumpart  31967  gsumhashmul  31968  symgcom2  32005  submarchi  32092  nsgmgc  32264  ghmqusker  32272  lmhmqusker  32273  rhmqusker  32278  idlinsubrg  32281  ply1degltdimlem  32404  fedgmullem1  32411  fedgmullem2  32412  fedgmul  32413  extdg1id  32439  madjusmdetlem1  32497  txomap  32504  rspectopn  32537  zarclssn  32543  zarcmplem  32551  cnvordtrestixx  32583  dya2iocucvr  32973  carsggect  33007  bnj1241  33508  bnj906  33631  fineqvac  33787  cvmscld  33954  fvline2  34807  cldregopn  34879  pibt2  35961  poimirlem15  36166  sstotbnd2  36306  totbndbnd  36321  heibor1  36342  heiborlem8  36350  lsmsat  37543  lssats  37547  lkrpssN  37698  dia2dimlem5  39604  cdlemn2a  39732  dihglblem6  39876  dochocsp  39915  dochdmj1  39926  dochsatshpb  39988  lcfl9a  40041  lclkrlem2r  40060  lclkrlem2s  40061  lclkrlem2v  40064  lcfrlem6  40083  lcfrlem25  40103  lcfrlem35  40113  mapdval2N  40166  mapdin  40198  baerlem5alem2  40247  baerlem5blem2  40248  mhphf  40829  dnnumch2  41430  oege1  41699  omabs2  41725  nadd2rabex  41779  clrellem  42016  iunrelexpmin1  42102  iunrelexpmin2  42106  dftrcl3  42114  brtrclfv2  42121  dfrtrcl3  42127  mnuprdlem1  42674  mnuprdlem2  42675  mullimc  43977  islptre  43980  mullimcf  43984  limcmptdm  43996  dvresntr  44279  itgperiod  44342  fourierdlem89  44556  fourierdlem91  44558  iccpartgt  45739  resmgmhm2  46213  setrecsres  47267