Theorem eqsstrrd 3944

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  3sstr3d  3963  ssxpb  6168  fnsnr  7173  suppssof1  8224  oaword1  8568  omword2  8590  oeeui  8619  nnaword1  8646  naddword1  8709  naddunif  8711  cantnfle  9679  cantnflem1d  9696  r1val1  9800  rankr1id  9885  rankxplim3  9905  ackbij2  10327  ttukeylem7  10600  gruima  10894  hashdmpropge2  14635  rlimi  15689  rlimi2  15690  lo1bdd  15696  o1bdd  15707  rlimuni  15726  rlimcld2  15754  o1co  15762  rlimcn1  15764  rlimcn3  15766  o1add2  15800  o1mul2  15801  o1sub2  15802  lo1add  15803  lo1mul  15804  o1dif  15806  rlimneg  15823  rlimsqzlem  15825  lo1le  15828  rlimno1  15830  ramub1lem1  17213  imasaddfnlem  17709  imasvscafn  17718  mrcidb  17798  mrieqv2d  17822  mreexexlem4d  17830  funcres  18080  funcsetcres2  18277  acsfiindd  18736  tsrdir  18787  resmgmhm2  18910  resmhm2  19026  ghmqusnsg  19505  ghmquskerlem3  19509  ghmqusker  19510  f1omvdco2  19671  sylow2a  19842  sylow3lem6  19855  dprdspan  20252  dprd2dlem2  20265  dprd2dlem1  20266  dprd2da  20267  dmdprdsplit2lem  20270  dprdsplit  20273  dpjcntz  20277  ablfac1eu  20298  ringidss  20515  subrg1  20843  subrgdvds  20847  subrguss  20848  subrginv  20849  drngdomn  21012  subdrgint  21069  primefld  21071  islss3  21243  lspsnneg  21290  lspextmo  21340  lspsnvs  21401  lsmcv  21428  islbs3  21442  rhmqusnsg  21590  f1lindf  22137  psrbaglesupp  22239  resspsrbas  22290  resspsradd  22291  resspsrmul  22292  evlseu  22401  evlsvvval  22411  epttop  23336  neitr  23507  ordtbas  23519  ordtrest2  23531  pnfnei  23547  mnfnei  23548  ordtrestixx  23549  dnsconst  23705  cmpcld  23729  txindis  23962  txtube  23968  xkohaus  23981  xkopt  23983  xkococnlem  23987  xkoinjcn  24015  qtopval2  24024  ssufl  24246  ufldom  24290  cnextcn  24395  tmdgsum2  24424  clssubg  24437  clsnsg  24438  ustund  24550  ustneism  24552  trust  24557  fmucnd  24619  imasdsf1olem  24701  setsmstopn  24806  metequiv2  24838  metust  24886  restmetu  24898  tngtopn  24978  xlebnum  25295  pi1xfrcnv  25387  limcdif  26205  limccnp  26220  limccnp2  26221  limcco  26222  dvn2bss  26259  cpnord  26264  dvcmulf  26274  dvmptres2  26291  dvmptcmul  26293  dvmptntr  26300  dvcnvrelem2  26347  dvcnvre  26348  taylthlem1  26709  taylthlem2  26710  ulmdvlem3  26738  psercnlem2  26760  rlimcxp  27310  o1cxp  27311  nosupbnd2lem1  28081  noinfbnd2lem1  28096  noetainflem4  28106  bdayiun  28310  negbday  28452  bdaypw2n0bndlem  28858  bdaypw2bnd  28860  bdayfinbndlem1  28862  lnssplng  29279  prlngpln4  29445  sspg  31339  ssps  31341  sspn  31347  mdslj1i  32930  mdslj2i  32931  sh1dle  32962  shatomistici  32972  sumdmdii  33026  prssad  33176  prssbd  33177  unidifsnel  33182  tpssad  33186  fisuppov1  33327  resf1o  33372  gsumpart  33674  gsumhashmul  33678  symgcom2  33695  submarchi  33797  nsgmgc  34013  lmhmqusker  34018  rhmquskerlem  34025  idlinsubrg  34031  ressply1evls1  34147  esplyind  34257  ply1degltdimlem  34304  fedgmullem1  34311  fedgmullem2  34312  fedgmul  34313  extdg1id  34348  fldextrspunlem1  34357  madjusmdetlem1  34509  txomap  34516  rspectopn  34549  zarclssn  34555  zarcmplem  34563  cnvordtrestixx  34595  dya2iocucvr  34966  carsggect  35000  bnj1241  35487  bnj906  35610  fineqvac  35852  cvmscld  36156  fvline2  37035  cldregopn  37243  ttcwf2  37437  pibt2  38477  poimirlem15  38690  sstotbnd2  38845  totbndbnd  38860  heibor1  38881  heiborlem8  38889  lsmsat  40202  lssats  40206  lkrpssN  40357  dia2dimlem5  42262  cdlemn2a  42390  dihglblem6  42534  dochocsp  42573  dochdmj1  42584  dochsatshpb  42646  lcfl9a  42699  lclkrlem2r  42718  lclkrlem2s  42719  lclkrlem2v  42722  lcfrlem6  42741  lcfrlem25  42761  lcfrlem35  42771  mapdval2N  42824  mapdin  42856  baerlem5alem2  42905  baerlem5blem2  42906  evlsbagval  43751  evlsmhpvvval  43760  mhphf  43762  dnnumch2  44189  oege1  44445  omabs2  44471  nadd2rabex  44525  clrellem  44759  iunrelexpmin1  44845  iunrelexpmin2  44849  dftrcl3  44857  brtrclfv2  44864  dfrtrcl3  44870  mnuprdlem1  45393  mnuprdlem2  45394  mullimc  46764  islptre  46767  mullimcf  46771  limcmptdm  46781  dvresntr  47064  itgperiod  47127  fourierdlem89  47341  fourierdlem91  47343  iccpartgt  48645  clnbgrgrim  49168  setrecsres  51006