Theorem eqsstrrd 4048

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  ssxpb  6205  fnsnr  7199  suppssof1  8240  oaword1  8608  omword2  8630  oeeui  8658  nnaword1  8685  naddword1  8747  naddunif  8749  cantnfle  9740  cantnflem1d  9757  r1val1  9855  rankr1id  9931  rankxplim3  9950  ackbij2  10311  ttukeylem7  10584  gruima  10871  hashdmpropge2  14532  rlimi  15559  rlimi2  15560  lo1bdd  15566  o1bdd  15577  rlimuni  15596  rlimcld2  15624  o1co  15632  rlimcn1  15634  rlimcn3  15636  o1add2  15670  o1mul2  15671  o1sub2  15672  lo1add  15673  lo1mul  15674  o1dif  15676  rlimneg  15695  rlimsqzlem  15697  lo1le  15700  rlimno1  15702  ramub1lem1  17073  imasaddfnlem  17588  imasvscafn  17597  mrcidb  17673  mrieqv2d  17697  mreexexlem4d  17705  funcres  17960  funcsetcres2  18160  acsfiindd  18623  tsrdir  18674  resmgmhm2  18750  resmhm2  18856  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  f1omvdco2  19490  sylow2a  19661  sylow3lem6  19674  dprdspan  20071  dprd2dlem2  20084  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  dprdsplit  20092  dpjcntz  20096  ablfac1eu  20117  ringidss  20300  subrg1  20610  subrgdvds  20614  subrguss  20615  subrginv  20616  drngdomn  20771  subdrgint  20826  primefld  20828  islss3  20980  lspsnneg  21027  lspextmo  21078  lspsnvs  21139  lsmcv  21166  islbs3  21180  rhmqusnsg  21318  f1lindf  21865  psrbaglesupp  21965  resspsrbas  22017  resspsradd  22018  resspsrmul  22019  evlseu  22130  epttop  23037  neitr  23209  ordtbas  23221  ordtrest2  23233  pnfnei  23249  mnfnei  23250  ordtrestixx  23251  dnsconst  23407  cmpcld  23431  txindis  23663  txtube  23669  xkohaus  23682  xkopt  23684  xkococnlem  23688  xkoinjcn  23716  qtopval2  23725  ssufl  23947  ufldom  23991  cnextcn  24096  tmdgsum2  24125  clssubg  24138  clsnsg  24139  ustund  24251  ustneism  24253  trust  24259  fmucnd  24322  imasdsf1olem  24404  setsmstopn  24511  metequiv2  24544  metust  24592  restmetu  24604  tngtopn  24692  xlebnum  25016  pi1xfrcnv  25109  limcdif  25931  limccnp  25946  limccnp2  25947  limcco  25948  dvn2bss  25986  cpnord  25991  dvcmulf  26002  dvmptres2  26020  dvmptcmul  26022  dvmptntr  26029  dvcnvrelem2  26077  dvcnvre  26078  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  psercnlem2  26486  rlimcxp  27035  o1cxp  27036  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetainflem4  27803  negsbday  28107  sspg  30760  ssps  30762  sspn  30768  mdslj1i  32351  mdslj2i  32352  sh1dle  32383  shatomistici  32393  sumdmdii  32447  unidifsnel  32563  resf1o  32744  gsumpart  33038  gsumhashmul  33040  symgcom2  33077  submarchi  33166  nsgmgc  33405  lmhmqusker  33410  rhmquskerlem  33418  idlinsubrg  33424  ply1degltdimlem  33635  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33676  madjusmdetlem1  33773  txomap  33780  rspectopn  33813  zarclssn  33819  zarcmplem  33827  cnvordtrestixx  33859  dya2iocucvr  34249  carsggect  34283  bnj1241  34783  bnj906  34906  fineqvac  35073  cvmscld  35241  fvline2  36110  cldregopn  36297  pibt2  37383  poimirlem15  37595  sstotbnd2  37734  totbndbnd  37749  heibor1  37770  heiborlem8  37778  lsmsat  38964  lssats  38968  lkrpssN  39119  dia2dimlem5  41025  cdlemn2a  41153  dihglblem6  41297  dochocsp  41336  dochdmj1  41347  dochsatshpb  41409  lcfl9a  41462  lclkrlem2r  41481  lclkrlem2s  41482  lclkrlem2v  41485  lcfrlem6  41504  lcfrlem25  41524  lcfrlem35  41534  mapdval2N  41587  mapdin  41619  baerlem5alem2  41668  baerlem5blem2  41669  evlsvvval  42518  evlsbagval  42521  evlsmhpvvval  42550  mhphf  42552  dnnumch2  43002  oege1  43268  omabs2  43294  nadd2rabex  43348  clrellem  43584  iunrelexpmin1  43670  iunrelexpmin2  43674  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  mnuprdlem1  44241  mnuprdlem2  44242  mullimc  45537  islptre  45540  mullimcf  45544  limcmptdm  45556  dvresntr  45839  itgperiod  45902  fourierdlem89  46116  fourierdlem91  46118  iccpartgt  47301  clnbgrgrim  47786  setrecsres  48794