Theorem eqsstrrd 3982

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  3sstr3d  4001  ssxpb  6147  fnsnr  7137  suppssof1  8178  oaword1  8516  omword2  8538  oeeui  8566  nnaword1  8593  naddword1  8655  naddunif  8657  cantnfle  9624  cantnflem1d  9641  r1val1  9739  rankr1id  9815  rankxplim3  9834  ackbij2  10195  ttukeylem7  10468  gruima  10755  hashdmpropge2  14448  rlimi  15479  rlimi2  15480  lo1bdd  15486  o1bdd  15497  rlimuni  15516  rlimcld2  15544  o1co  15552  rlimcn1  15554  rlimcn3  15556  o1add2  15590  o1mul2  15591  o1sub2  15592  lo1add  15593  lo1mul  15594  o1dif  15596  rlimneg  15613  rlimsqzlem  15615  lo1le  15618  rlimno1  15620  ramub1lem1  16997  imasaddfnlem  17491  imasvscafn  17500  mrcidb  17576  mrieqv2d  17600  mreexexlem4d  17608  funcres  17858  funcsetcres2  18055  acsfiindd  18512  tsrdir  18563  resmgmhm2  18639  resmhm2  18748  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  f1omvdco2  19378  sylow2a  19549  sylow3lem6  19562  dprdspan  19959  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  dprdsplit  19980  dpjcntz  19984  ablfac1eu  20005  ringidss  20186  subrg1  20491  subrgdvds  20495  subrguss  20496  subrginv  20497  drngdomn  20658  subdrgint  20712  primefld  20714  islss3  20865  lspsnneg  20912  lspextmo  20963  lspsnvs  21024  lsmcv  21051  islbs3  21065  rhmqusnsg  21195  f1lindf  21731  psrbaglesupp  21831  resspsrbas  21883  resspsradd  21884  resspsrmul  21885  evlseu  21990  epttop  22896  neitr  23067  ordtbas  23079  ordtrest2  23091  pnfnei  23107  mnfnei  23108  ordtrestixx  23109  dnsconst  23265  cmpcld  23289  txindis  23521  txtube  23527  xkohaus  23540  xkopt  23542  xkococnlem  23546  xkoinjcn  23574  qtopval2  23583  ssufl  23805  ufldom  23849  cnextcn  23954  tmdgsum2  23983  clssubg  23996  clsnsg  23997  ustund  24109  ustneism  24111  trust  24117  fmucnd  24179  imasdsf1olem  24261  setsmstopn  24366  metequiv2  24398  metust  24446  restmetu  24458  tngtopn  24538  xlebnum  24864  pi1xfrcnv  24957  limcdif  25777  limccnp  25792  limccnp2  25793  limcco  25794  dvn2bss  25832  cpnord  25837  dvcmulf  25848  dvmptres2  25866  dvmptcmul  25868  dvmptntr  25875  dvcnvrelem2  25923  dvcnvre  25924  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem3  26311  psercnlem2  26334  rlimcxp  26884  o1cxp  26885  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetainflem4  27652  negsbday  27963  sspg  30657  ssps  30659  sspn  30665  mdslj1i  32248  mdslj2i  32249  sh1dle  32280  shatomistici  32290  sumdmdii  32344  prssad  32458  prssbd  32459  unidifsnel  32464  tpssad  32468  fisuppov1  32606  resf1o  32653  gsumpart  32997  gsumhashmul  33001  symgcom2  33041  submarchi  33140  nsgmgc  33383  lmhmqusker  33388  rhmquskerlem  33396  idlinsubrg  33402  ressply1evls1  33534  ply1degltdimlem  33618  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  extdg1id  33661  fldextrspunlem1  33670  madjusmdetlem1  33817  txomap  33824  rspectopn  33857  zarclssn  33863  zarcmplem  33871  cnvordtrestixx  33903  dya2iocucvr  34275  carsggect  34309  bnj1241  34797  bnj906  34920  fineqvac  35087  cvmscld  35260  fvline2  36134  cldregopn  36319  pibt2  37405  poimirlem15  37629  sstotbnd2  37768  totbndbnd  37783  heibor1  37804  heiborlem8  37812  lsmsat  39001  lssats  39005  lkrpssN  39156  dia2dimlem5  41062  cdlemn2a  41190  dihglblem6  41334  dochocsp  41373  dochdmj1  41384  dochsatshpb  41446  lcfl9a  41499  lclkrlem2r  41518  lclkrlem2s  41519  lclkrlem2v  41522  lcfrlem6  41541  lcfrlem25  41561  lcfrlem35  41571  mapdval2N  41624  mapdin  41656  baerlem5alem2  41705  baerlem5blem2  41706  evlsvvval  42551  evlsbagval  42554  evlsmhpvvval  42583  mhphf  42585  dnnumch2  43034  oege1  43295  omabs2  43321  nadd2rabex  43375  clrellem  43611  iunrelexpmin1  43697  iunrelexpmin2  43701  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  mnuprdlem1  44261  mnuprdlem2  44262  mullimc  45614  islptre  45617  mullimcf  45621  limcmptdm  45633  dvresntr  45916  itgperiod  45979  fourierdlem89  46193  fourierdlem91  46195  iccpartgt  47428  clnbgrgrim  47934  setrecsres  49691