Theorem eqsstrrd 3971

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

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

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 3920

This theorem is referenced by:  3sstr3d  3990  ssxpb  6123  fnsnr  7099  suppssof1  8132  oaword1  8470  omword2  8492  oeeui  8520  nnaword1  8547  naddword1  8609  naddunif  8611  cantnfle  9567  cantnflem1d  9584  r1val1  9682  rankr1id  9758  rankxplim3  9777  ackbij2  10136  ttukeylem7  10409  gruima  10696  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  18586  resmhm2  18695  ghmqusnsg  19161  ghmquskerlem3  19165  ghmqusker  19166  f1omvdco2  19327  sylow2a  19498  sylow3lem6  19511  dprdspan  19908  dprd2dlem2  19921  dprd2dlem1  19922  dprd2da  19923  dmdprdsplit2lem  19926  dprdsplit  19929  dpjcntz  19933  ablfac1eu  19954  ringidss  20162  subrg1  20467  subrgdvds  20471  subrguss  20472  subrginv  20473  drngdomn  20634  subdrgint  20688  primefld  20690  islss3  20862  lspsnneg  20909  lspextmo  20960  lspsnvs  21021  lsmcv  21048  islbs3  21062  rhmqusnsg  21192  f1lindf  21729  psrbaglesupp  21829  resspsrbas  21881  resspsradd  21882  resspsrmul  21883  evlseu  21988  epttop  22894  neitr  23065  ordtbas  23077  ordtrest2  23089  pnfnei  23105  mnfnei  23106  ordtrestixx  23107  dnsconst  23263  cmpcld  23287  txindis  23519  txtube  23525  xkohaus  23538  xkopt  23540  xkococnlem  23544  xkoinjcn  23572  qtopval2  23581  ssufl  23803  ufldom  23847  cnextcn  23952  tmdgsum2  23981  clssubg  23994  clsnsg  23995  ustund  24107  ustneism  24109  trust  24115  fmucnd  24177  imasdsf1olem  24259  setsmstopn  24364  metequiv2  24396  metust  24444  restmetu  24456  tngtopn  24536  xlebnum  24862  pi1xfrcnv  24955  limcdif  25775  limccnp  25790  limccnp2  25791  limcco  25792  dvn2bss  25830  cpnord  25835  dvcmulf  25846  dvmptres2  25864  dvmptcmul  25866  dvmptntr  25873  dvcnvrelem2  25921  dvcnvre  25922  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem3  26309  psercnlem2  26332  rlimcxp  26882  o1cxp  26883  nosupbnd2lem1  27625  noinfbnd2lem1  27640  noetainflem4  27650  bdayiun  27829  negsbday  27968  sspg  30672  ssps  30674  sspn  30680  mdslj1i  32263  mdslj2i  32264  sh1dle  32295  shatomistici  32305  sumdmdii  32359  prssad  32473  prssbd  32474  unidifsnel  32479  tpssad  32483  fisuppov1  32625  resf1o  32673  gsumpart  33010  gsumhashmul  33014  symgcom2  33026  submarchi  33128  nsgmgc  33349  lmhmqusker  33354  rhmquskerlem  33362  idlinsubrg  33368  ressply1evls1  33500  ply1degltdimlem  33589  fedgmullem1  33596  fedgmullem2  33597  fedgmul  33598  extdg1id  33633  fldextrspunlem1  33642  madjusmdetlem1  33794  txomap  33801  rspectopn  33834  zarclssn  33840  zarcmplem  33848  cnvordtrestixx  33880  dya2iocucvr  34252  carsggect  34286  bnj1241  34774  bnj906  34897  fineqvac  35072  cvmscld  35250  fvline2  36124  cldregopn  36309  pibt2  37395  poimirlem15  37619  sstotbnd2  37758  totbndbnd  37773  heibor1  37794  heiborlem8  37802  lsmsat  38991  lssats  38995  lkrpssN  39146  dia2dimlem5  41051  cdlemn2a  41179  dihglblem6  41323  dochocsp  41362  dochdmj1  41373  dochsatshpb  41435  lcfl9a  41488  lclkrlem2r  41507  lclkrlem2s  41508  lclkrlem2v  41511  lcfrlem6  41530  lcfrlem25  41550  lcfrlem35  41560  mapdval2N  41613  mapdin  41645  baerlem5alem2  41694  baerlem5blem2  41695  evlsvvval  42540  evlsbagval  42543  evlsmhpvvval  42572  mhphf  42574  dnnumch2  43022  oege1  43283  omabs2  43309  nadd2rabex  43363  clrellem  43599  iunrelexpmin1  43685  iunrelexpmin2  43689  dftrcl3  43697  brtrclfv2  43704  dfrtrcl3  43710  mnuprdlem1  44249  mnuprdlem2  44250  mullimc  45601  islptre  45604  mullimcf  45608  limcmptdm  45620  dvresntr  45903  itgperiod  45966  fourierdlem89  46180  fourierdlem91  46182  iccpartgt  47415  clnbgrgrim  47922  setrecsres  49691