Theorem eqsstrrd 3985

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

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

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 2702

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

This theorem is referenced by:  3sstr3d  4004  ssxpb  6150  fnsnr  7140  suppssof1  8181  oaword1  8519  omword2  8541  oeeui  8569  nnaword1  8596  naddword1  8658  naddunif  8660  cantnfle  9631  cantnflem1d  9648  r1val1  9746  rankr1id  9822  rankxplim3  9841  ackbij2  10202  ttukeylem7  10475  gruima  10762  hashdmpropge2  14455  rlimi  15486  rlimi2  15487  lo1bdd  15493  o1bdd  15504  rlimuni  15523  rlimcld2  15551  o1co  15559  rlimcn1  15561  rlimcn3  15563  o1add2  15597  o1mul2  15598  o1sub2  15599  lo1add  15600  lo1mul  15601  o1dif  15603  rlimneg  15620  rlimsqzlem  15622  lo1le  15625  rlimno1  15627  ramub1lem1  17004  imasaddfnlem  17498  imasvscafn  17507  mrcidb  17583  mrieqv2d  17607  mreexexlem4d  17615  funcres  17865  funcsetcres2  18062  acsfiindd  18519  tsrdir  18570  resmgmhm2  18646  resmhm2  18755  ghmqusnsg  19221  ghmquskerlem3  19225  ghmqusker  19226  f1omvdco2  19385  sylow2a  19556  sylow3lem6  19569  dprdspan  19966  dprd2dlem2  19979  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  dprdsplit  19987  dpjcntz  19991  ablfac1eu  20012  ringidss  20193  subrg1  20498  subrgdvds  20502  subrguss  20503  subrginv  20504  drngdomn  20665  subdrgint  20719  primefld  20721  islss3  20872  lspsnneg  20919  lspextmo  20970  lspsnvs  21031  lsmcv  21058  islbs3  21072  rhmqusnsg  21202  f1lindf  21738  psrbaglesupp  21838  resspsrbas  21890  resspsradd  21891  resspsrmul  21892  evlseu  21997  epttop  22903  neitr  23074  ordtbas  23086  ordtrest2  23098  pnfnei  23114  mnfnei  23115  ordtrestixx  23116  dnsconst  23272  cmpcld  23296  txindis  23528  txtube  23534  xkohaus  23547  xkopt  23549  xkococnlem  23553  xkoinjcn  23581  qtopval2  23590  ssufl  23812  ufldom  23856  cnextcn  23961  tmdgsum2  23990  clssubg  24003  clsnsg  24004  ustund  24116  ustneism  24118  trust  24124  fmucnd  24186  imasdsf1olem  24268  setsmstopn  24373  metequiv2  24405  metust  24453  restmetu  24465  tngtopn  24545  xlebnum  24871  pi1xfrcnv  24964  limcdif  25784  limccnp  25799  limccnp2  25800  limcco  25801  dvn2bss  25839  cpnord  25844  dvcmulf  25855  dvmptres2  25873  dvmptcmul  25875  dvmptntr  25882  dvcnvrelem2  25930  dvcnvre  25931  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem3  26318  psercnlem2  26341  rlimcxp  26891  o1cxp  26892  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetainflem4  27659  negsbday  27970  sspg  30664  ssps  30666  sspn  30672  mdslj1i  32255  mdslj2i  32256  sh1dle  32287  shatomistici  32297  sumdmdii  32351  prssad  32465  prssbd  32466  unidifsnel  32471  tpssad  32475  fisuppov1  32613  resf1o  32660  gsumpart  33004  gsumhashmul  33008  symgcom2  33048  submarchi  33147  nsgmgc  33390  lmhmqusker  33395  rhmquskerlem  33403  idlinsubrg  33409  ressply1evls1  33541  ply1degltdimlem  33625  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdg1id  33668  fldextrspunlem1  33677  madjusmdetlem1  33824  txomap  33831  rspectopn  33864  zarclssn  33870  zarcmplem  33878  cnvordtrestixx  33910  dya2iocucvr  34282  carsggect  34316  bnj1241  34804  bnj906  34927  fineqvac  35094  cvmscld  35267  fvline2  36141  cldregopn  36326  pibt2  37412  poimirlem15  37636  sstotbnd2  37775  totbndbnd  37790  heibor1  37811  heiborlem8  37819  lsmsat  39008  lssats  39012  lkrpssN  39163  dia2dimlem5  41069  cdlemn2a  41197  dihglblem6  41341  dochocsp  41380  dochdmj1  41391  dochsatshpb  41453  lcfl9a  41506  lclkrlem2r  41525  lclkrlem2s  41526  lclkrlem2v  41529  lcfrlem6  41548  lcfrlem25  41568  lcfrlem35  41578  mapdval2N  41631  mapdin  41663  baerlem5alem2  41712  baerlem5blem2  41713  evlsvvval  42558  evlsbagval  42561  evlsmhpvvval  42590  mhphf  42592  dnnumch2  43041  oege1  43302  omabs2  43328  nadd2rabex  43382  clrellem  43618  iunrelexpmin1  43704  iunrelexpmin2  43708  dftrcl3  43716  brtrclfv2  43723  dfrtrcl3  43729  mnuprdlem1  44268  mnuprdlem2  44269  mullimc  45621  islptre  45624  mullimcf  45628  limcmptdm  45640  dvresntr  45923  itgperiod  45986  fourierdlem89  46200  fourierdlem91  46202  iccpartgt  47432  clnbgrgrim  47938  setrecsres  49695