Theorem eqsstrrd 3965

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 3964	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  3sstr3d  3984  ssxpb  6121  fnsnr  7097  suppssof1  8129  oaword1  8467  omword2  8489  oeeui  8517  nnaword1  8544  naddword1  8606  naddunif  8608  cantnfle  9561  cantnflem1d  9578  r1val1  9679  rankr1id  9755  rankxplim3  9774  ackbij2  10133  ttukeylem7  10406  gruima  10693  hashdmpropge2  14390  rlimi  15420  rlimi2  15421  lo1bdd  15427  o1bdd  15438  rlimuni  15457  rlimcld2  15485  o1co  15493  rlimcn1  15495  rlimcn3  15497  o1add2  15531  o1mul2  15532  o1sub2  15533  lo1add  15534  lo1mul  15535  o1dif  15537  rlimneg  15554  rlimsqzlem  15556  lo1le  15559  rlimno1  15561  ramub1lem1  16938  imasaddfnlem  17432  imasvscafn  17441  mrcidb  17521  mrieqv2d  17545  mreexexlem4d  17553  funcres  17803  funcsetcres2  18000  acsfiindd  18459  tsrdir  18510  resmgmhm2  18620  resmhm2  18729  ghmqusnsg  19194  ghmquskerlem3  19198  ghmqusker  19199  f1omvdco2  19360  sylow2a  19531  sylow3lem6  19544  dprdspan  19941  dprd2dlem2  19954  dprd2dlem1  19955  dprd2da  19956  dmdprdsplit2lem  19959  dprdsplit  19962  dpjcntz  19966  ablfac1eu  19987  ringidss  20195  subrg1  20497  subrgdvds  20501  subrguss  20502  subrginv  20503  drngdomn  20664  subdrgint  20718  primefld  20720  islss3  20892  lspsnneg  20939  lspextmo  20990  lspsnvs  21051  lsmcv  21078  islbs3  21092  rhmqusnsg  21222  f1lindf  21759  psrbaglesupp  21859  resspsrbas  21911  resspsradd  21912  resspsrmul  21913  evlseu  22018  epttop  22924  neitr  23095  ordtbas  23107  ordtrest2  23119  pnfnei  23135  mnfnei  23136  ordtrestixx  23137  dnsconst  23293  cmpcld  23317  txindis  23549  txtube  23555  xkohaus  23568  xkopt  23570  xkococnlem  23574  xkoinjcn  23602  qtopval2  23611  ssufl  23833  ufldom  23877  cnextcn  23982  tmdgsum2  24011  clssubg  24024  clsnsg  24025  ustund  24137  ustneism  24139  trust  24144  fmucnd  24206  imasdsf1olem  24288  setsmstopn  24393  metequiv2  24425  metust  24473  restmetu  24485  tngtopn  24565  xlebnum  24891  pi1xfrcnv  24984  limcdif  25804  limccnp  25819  limccnp2  25820  limcco  25821  dvn2bss  25859  cpnord  25864  dvcmulf  25875  dvmptres2  25893  dvmptcmul  25895  dvmptntr  25902  dvcnvrelem2  25950  dvcnvre  25951  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem3  26338  psercnlem2  26361  rlimcxp  26911  o1cxp  26912  nosupbnd2lem1  27654  noinfbnd2lem1  27669  noetainflem4  27679  bdayiun  27860  negsbday  27999  sspg  30708  ssps  30710  sspn  30716  mdslj1i  32299  mdslj2i  32300  sh1dle  32331  shatomistici  32341  sumdmdii  32395  prssad  32509  prssbd  32510  unidifsnel  32515  tpssad  32519  fisuppov1  32664  resf1o  32713  gsumpart  33037  gsumhashmul  33041  symgcom2  33053  submarchi  33155  nsgmgc  33377  lmhmqusker  33382  rhmquskerlem  33390  idlinsubrg  33396  ressply1evls1  33528  ply1degltdimlem  33635  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33679  fldextrspunlem1  33688  madjusmdetlem1  33840  txomap  33847  rspectopn  33880  zarclssn  33886  zarcmplem  33894  cnvordtrestixx  33926  dya2iocucvr  34297  carsggect  34331  bnj1241  34819  bnj906  34942  fineqvac  35139  cvmscld  35317  fvline2  36190  cldregopn  36375  pibt2  37461  poimirlem15  37685  sstotbnd2  37824  totbndbnd  37839  heibor1  37860  heiborlem8  37868  lsmsat  39117  lssats  39121  lkrpssN  39272  dia2dimlem5  41177  cdlemn2a  41305  dihglblem6  41449  dochocsp  41488  dochdmj1  41499  dochsatshpb  41561  lcfl9a  41614  lclkrlem2r  41633  lclkrlem2s  41634  lclkrlem2v  41637  lcfrlem6  41656  lcfrlem25  41676  lcfrlem35  41686  mapdval2N  41739  mapdin  41771  baerlem5alem2  41820  baerlem5blem2  41821  evlsvvval  42666  evlsbagval  42669  evlsmhpvvval  42698  mhphf  42700  dnnumch2  43148  oege1  43409  omabs2  43435  nadd2rabex  43489  clrellem  43725  iunrelexpmin1  43811  iunrelexpmin2  43815  dftrcl3  43823  brtrclfv2  43830  dfrtrcl3  43836  mnuprdlem1  44375  mnuprdlem2  44376  mullimc  45726  islptre  45729  mullimcf  45733  limcmptdm  45743  dvresntr  46026  itgperiod  46089  fourierdlem89  46303  fourierdlem91  46305  iccpartgt  47537  clnbgrgrim  48044  setrecsres  49813