Theorem eqsstrrd 3994

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  3sstr3d  4013  ssxpb  6163  fnsnr  7155  suppssof1  8198  oaword1  8564  omword2  8586  oeeui  8614  nnaword1  8641  naddword1  8703  naddunif  8705  cantnfle  9685  cantnflem1d  9702  r1val1  9800  rankr1id  9876  rankxplim3  9895  ackbij2  10256  ttukeylem7  10529  gruima  10816  hashdmpropge2  14501  rlimi  15529  rlimi2  15530  lo1bdd  15536  o1bdd  15547  rlimuni  15566  rlimcld2  15594  o1co  15602  rlimcn1  15604  rlimcn3  15606  o1add2  15640  o1mul2  15641  o1sub2  15642  lo1add  15643  lo1mul  15644  o1dif  15646  rlimneg  15663  rlimsqzlem  15665  lo1le  15668  rlimno1  15670  ramub1lem1  17046  imasaddfnlem  17542  imasvscafn  17551  mrcidb  17627  mrieqv2d  17651  mreexexlem4d  17659  funcres  17909  funcsetcres2  18106  acsfiindd  18563  tsrdir  18614  resmgmhm2  18690  resmhm2  18799  ghmqusnsg  19265  ghmquskerlem3  19269  ghmqusker  19270  f1omvdco2  19429  sylow2a  19600  sylow3lem6  19613  dprdspan  20010  dprd2dlem2  20023  dprd2dlem1  20024  dprd2da  20025  dmdprdsplit2lem  20028  dprdsplit  20031  dpjcntz  20035  ablfac1eu  20056  ringidss  20237  subrg1  20542  subrgdvds  20546  subrguss  20547  subrginv  20548  drngdomn  20709  subdrgint  20763  primefld  20765  islss3  20916  lspsnneg  20963  lspextmo  21014  lspsnvs  21075  lsmcv  21102  islbs3  21116  rhmqusnsg  21246  f1lindf  21782  psrbaglesupp  21882  resspsrbas  21934  resspsradd  21935  resspsrmul  21936  evlseu  22041  epttop  22947  neitr  23118  ordtbas  23130  ordtrest2  23142  pnfnei  23158  mnfnei  23159  ordtrestixx  23160  dnsconst  23316  cmpcld  23340  txindis  23572  txtube  23578  xkohaus  23591  xkopt  23593  xkococnlem  23597  xkoinjcn  23625  qtopval2  23634  ssufl  23856  ufldom  23900  cnextcn  24005  tmdgsum2  24034  clssubg  24047  clsnsg  24048  ustund  24160  ustneism  24162  trust  24168  fmucnd  24230  imasdsf1olem  24312  setsmstopn  24417  metequiv2  24449  metust  24497  restmetu  24509  tngtopn  24589  xlebnum  24915  pi1xfrcnv  25008  limcdif  25829  limccnp  25844  limccnp2  25845  limcco  25846  dvn2bss  25884  cpnord  25889  dvcmulf  25900  dvmptres2  25918  dvmptcmul  25920  dvmptntr  25927  dvcnvrelem2  25975  dvcnvre  25976  taylthlem1  26333  taylthlem2  26334  taylthlem2OLD  26335  ulmdvlem3  26363  psercnlem2  26386  rlimcxp  26936  o1cxp  26937  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetainflem4  27704  negsbday  28015  sspg  30709  ssps  30711  sspn  30717  mdslj1i  32300  mdslj2i  32301  sh1dle  32332  shatomistici  32342  sumdmdii  32396  prssad  32510  prssbd  32511  unidifsnel  32516  tpssad  32520  fisuppov1  32660  resf1o  32707  gsumpart  33051  gsumhashmul  33055  symgcom2  33095  submarchi  33184  nsgmgc  33427  lmhmqusker  33432  rhmquskerlem  33440  idlinsubrg  33446  ressply1evls1  33578  ply1degltdimlem  33662  fedgmullem1  33669  fedgmullem2  33670  fedgmul  33671  extdg1id  33707  fldextrspunlem1  33716  madjusmdetlem1  33858  txomap  33865  rspectopn  33898  zarclssn  33904  zarcmplem  33912  cnvordtrestixx  33944  dya2iocucvr  34316  carsggect  34350  bnj1241  34838  bnj906  34961  fineqvac  35128  cvmscld  35295  fvline2  36164  cldregopn  36349  pibt2  37435  poimirlem15  37659  sstotbnd2  37798  totbndbnd  37813  heibor1  37834  heiborlem8  37842  lsmsat  39026  lssats  39030  lkrpssN  39181  dia2dimlem5  41087  cdlemn2a  41215  dihglblem6  41359  dochocsp  41398  dochdmj1  41409  dochsatshpb  41471  lcfl9a  41524  lclkrlem2r  41543  lclkrlem2s  41544  lclkrlem2v  41547  lcfrlem6  41566  lcfrlem25  41586  lcfrlem35  41596  mapdval2N  41649  mapdin  41681  baerlem5alem2  41730  baerlem5blem2  41731  evlsvvval  42586  evlsbagval  42589  evlsmhpvvval  42618  mhphf  42620  dnnumch2  43069  oege1  43330  omabs2  43356  nadd2rabex  43410  clrellem  43646  iunrelexpmin1  43732  iunrelexpmin2  43736  dftrcl3  43744  brtrclfv2  43751  dfrtrcl3  43757  mnuprdlem1  44296  mnuprdlem2  44297  mullimc  45645  islptre  45648  mullimcf  45652  limcmptdm  45664  dvresntr  45947  itgperiod  46010  fourierdlem89  46224  fourierdlem91  46226  iccpartgt  47441  clnbgrgrim  47947  setrecsres  49566