Theorem eqsstrrd 3980

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  3sstr3d  3999  ssxpb  6173  fnsnr  7162  suppssof1  8195  oaword1  8537  omword2  8559  oeeui  8588  nnaword1  8615  naddword1  8678  naddunif  8680  cantnfle  9640  cantnflem1d  9657  r1val1  9758  rankr1id  9834  rankxplim3  9853  ackbij2  10225  ttukeylem7  10499  gruima  10787  hashdmpropge2  14520  rlimi  15564  rlimi2  15565  lo1bdd  15571  o1bdd  15582  rlimuni  15601  rlimcld2  15629  o1co  15637  rlimcn1  15639  rlimcn3  15641  o1add2  15675  o1mul2  15676  o1sub2  15677  lo1add  15678  lo1mul  15679  o1dif  15681  rlimneg  15698  rlimsqzlem  15700  lo1le  15703  rlimno1  15705  ramub1lem1  17086  imasaddfnlem  17582  imasvscafn  17591  mrcidb  17671  mrieqv2d  17695  mreexexlem4d  17703  funcres  17953  funcsetcres2  18150  acsfiindd  18609  tsrdir  18660  resmgmhm2  18770  resmhm2  18880  ghmqusnsg  19352  ghmquskerlem3  19356  ghmqusker  19357  f1omvdco2  19518  sylow2a  19689  sylow3lem6  19702  dprdspan  20099  dprd2dlem2  20112  dprd2dlem1  20113  dprd2da  20114  dmdprdsplit2lem  20117  dprdsplit  20120  dpjcntz  20124  ablfac1eu  20145  ringidss  20360  subrg1  20667  subrgdvds  20671  subrguss  20672  subrginv  20673  drngdomn  20833  subdrgint  20884  primefld  20886  islss3  21058  lspsnneg  21105  lspextmo  21155  lspsnvs  21216  lsmcv  21243  islbs3  21257  rhmqusnsg  21396  f1lindf  21941  psrbaglesupp  22041  resspsrbas  22092  resspsradd  22093  resspsrmul  22094  evlseu  22203  evlsvvval  22213  epttop  23135  neitr  23306  ordtbas  23318  ordtrest2  23330  pnfnei  23346  mnfnei  23347  ordtrestixx  23348  dnsconst  23504  cmpcld  23528  txindis  23760  txtube  23766  xkohaus  23779  xkopt  23781  xkococnlem  23785  xkoinjcn  23813  qtopval2  23822  ssufl  24044  ufldom  24088  cnextcn  24193  tmdgsum2  24222  clssubg  24235  clsnsg  24236  ustund  24348  ustneism  24350  trust  24355  fmucnd  24417  imasdsf1olem  24499  setsmstopn  24604  metequiv2  24636  metust  24684  restmetu  24696  tngtopn  24776  xlebnum  25093  pi1xfrcnv  25185  limcdif  26004  limccnp  26019  limccnp2  26020  limcco  26021  dvn2bss  26058  cpnord  26063  dvcmulf  26073  dvmptres2  26090  dvmptcmul  26092  dvmptntr  26099  dvcnvrelem2  26146  dvcnvre  26147  taylthlem1  26502  taylthlem2  26503  ulmdvlem3  26531  psercnlem2  26553  rlimcxp  27104  o1cxp  27105  nosupbnd2lem1  27845  noinfbnd2lem1  27860  noetainflem4  27870  bdayiun  28074  negbday  28216  bdaypw2n0bndlem  28622  bdaypw2bnd  28624  bdayfinbndlem1  28626  lnssplng  29032  sspg  31021  ssps  31023  sspn  31029  mdslj1i  32612  mdslj2i  32613  sh1dle  32644  shatomistici  32654  sumdmdii  32708  prssad  32816  prssbd  32817  unidifsnel  32822  tpssad  32826  fisuppov1  32969  resf1o  33016  gsumpart  33324  gsumhashmul  33328  symgcom2  33345  submarchi  33447  nsgmgc  33665  lmhmqusker  33670  rhmquskerlem  33677  idlinsubrg  33683  ressply1evls1  33800  esplyind  33910  ply1degltdimlem  33957  fedgmullem1  33964  fedgmullem2  33965  fedgmul  33966  extdg1id  34001  fldextrspunlem1  34010  madjusmdetlem1  34162  txomap  34169  rspectopn  34202  zarclssn  34208  zarcmplem  34216  cnvordtrestixx  34248  dya2iocucvr  34619  carsggect  34653  bnj1241  35140  bnj906  35263  fineqvac  35452  cvmscld  35664  fvline2  36537  cldregopn  36731  ttcwf2  36925  pibt2  37951  poimirlem15  38174  sstotbnd2  38313  totbndbnd  38328  heibor1  38349  heiborlem8  38357  lsmsat  39672  lssats  39676  lkrpssN  39827  dia2dimlem5  41732  cdlemn2a  41860  dihglblem6  42004  dochocsp  42043  dochdmj1  42054  dochsatshpb  42116  lcfl9a  42169  lclkrlem2r  42188  lclkrlem2s  42189  lclkrlem2v  42192  lcfrlem6  42211  lcfrlem25  42231  lcfrlem35  42241  mapdval2N  42294  mapdin  42326  baerlem5alem2  42375  baerlem5blem2  42376  evlsbagval  43210  evlsmhpvvval  43219  mhphf  43221  dnnumch2  43664  oege1  43925  omabs2  43951  nadd2rabex  44005  clrellem  44240  iunrelexpmin1  44326  iunrelexpmin2  44330  dftrcl3  44338  brtrclfv2  44345  dfrtrcl3  44351  mnuprdlem1  44874  mnuprdlem2  44875  mullimc  46224  islptre  46227  mullimcf  46231  limcmptdm  46241  dvresntr  46524  itgperiod  46587  fourierdlem89  46801  fourierdlem91  46803  iccpartgt  48065  clnbgrgrim  48588  setrecsres  50365