MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstrrd Structured version   Visualization version   GIF version

Theorem eqsstrrd 3988
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
StepHypRef Expression
1 eqsstrrd.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2743 . 2 (𝜑𝐴 = 𝐵)
3 eqsstrrd.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 3987 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  ssxpb  6131  fnsnr  7116  suppssof1  8135  oaword1  8504  omword2  8526  oeeui  8554  nnaword1  8581  naddword1  8642  naddunif  8644  cantnfle  9614  cantnflem1d  9631  r1val1  9729  rankr1id  9805  rankxplim3  9824  ackbij2  10186  ttukeylem7  10458  gruima  10745  hashdmpropge2  14389  rlimi  15402  rlimi2  15403  lo1bdd  15409  o1bdd  15420  rlimuni  15439  rlimcld2  15467  o1co  15475  rlimcn1  15477  rlimcn3  15479  o1add2  15513  o1mul2  15514  o1sub2  15515  lo1add  15516  lo1mul  15517  o1dif  15519  rlimneg  15538  rlimsqzlem  15540  lo1le  15543  rlimno1  15545  ramub1lem1  16905  imasaddfnlem  17417  imasvscafn  17426  mrcidb  17502  mrieqv2d  17526  mreexexlem4d  17534  funcres  17789  funcsetcres2  17986  acsfiindd  18449  tsrdir  18500  resmhm2  18639  f1omvdco2  19237  sylow2a  19408  sylow3lem6  19421  dprdspan  19813  dprd2dlem2  19826  dprd2dlem1  19827  dprd2da  19828  dmdprdsplit2lem  19831  dprdsplit  19834  dpjcntz  19838  ablfac1eu  19859  ringidss  20005  subrg1  20248  subrgdvds  20252  subrguss  20253  subrginv  20254  subdrgint  20286  primefld  20288  islss3  20436  lspsnneg  20483  lspextmo  20533  lspsnvs  20591  lsmcv  20618  islbs3  20632  drngdomn  20789  f1lindf  21244  psrbaglesupp  21342  psrbaglesuppOLD  21343  resspsrbas  21400  resspsradd  21401  resspsrmul  21402  evlseu  21509  epttop  22375  neitr  22547  ordtbas  22559  ordtrest2  22571  pnfnei  22587  mnfnei  22588  ordtrestixx  22589  dnsconst  22745  cmpcld  22769  txindis  23001  txtube  23007  xkohaus  23020  xkopt  23022  xkococnlem  23026  xkoinjcn  23054  qtopval2  23063  ssufl  23285  ufldom  23329  cnextcn  23434  tmdgsum2  23463  clssubg  23476  clsnsg  23477  ustund  23589  ustneism  23591  trust  23597  fmucnd  23660  imasdsf1olem  23742  setsmstopn  23849  metequiv2  23882  metust  23930  restmetu  23942  tngtopn  24030  xlebnum  24344  pi1xfrcnv  24436  limcdif  25256  limccnp  25271  limccnp2  25272  limcco  25273  dvn2bss  25310  cpnord  25315  dvcmulf  25325  dvmptres2  25342  dvmptcmul  25344  dvmptntr  25351  dvcnvrelem2  25398  dvcnvre  25399  taylthlem1  25748  taylthlem2  25749  ulmdvlem3  25777  psercnlem2  25799  rlimcxp  26339  o1cxp  26340  nosupbnd2lem1  27079  noinfbnd2lem1  27094  noetainflem4  27104  sspg  29712  ssps  29714  sspn  29720  mdslj1i  31303  mdslj2i  31304  sh1dle  31335  shatomistici  31345  sumdmdii  31399  unidifsnel  31504  resf1o  31689  gsumpart  31939  gsumhashmul  31940  symgcom2  31977  submarchi  32064  nsgmgc  32230  ghmqusker  32238  idlinsubrg  32245  fedgmullem1  32364  fedgmullem2  32365  fedgmul  32366  extdg1id  32392  madjusmdetlem1  32448  txomap  32455  rspectopn  32488  zarclssn  32494  zarcmplem  32502  cnvordtrestixx  32534  dya2iocucvr  32924  carsggect  32958  bnj1241  33459  bnj906  33582  fineqvac  33738  cvmscld  33907  fvline2  34760  cldregopn  34832  pibt2  35917  poimirlem15  36122  sstotbnd2  36262  totbndbnd  36277  heibor1  36298  heiborlem8  36306  lsmsat  37499  lssats  37503  lkrpssN  37654  dia2dimlem5  39560  cdlemn2a  39688  dihglblem6  39832  dochocsp  39871  dochdmj1  39882  dochsatshpb  39944  lcfl9a  39997  lclkrlem2r  40016  lclkrlem2s  40017  lclkrlem2v  40020  lcfrlem6  40039  lcfrlem25  40059  lcfrlem35  40069  mapdval2N  40122  mapdin  40154  baerlem5alem2  40203  baerlem5blem2  40204  mhphf  40800  dnnumch2  41401  oege1  41670  omabs2  41696  nadd2rabex  41731  clrellem  41968  iunrelexpmin1  42054  iunrelexpmin2  42058  dftrcl3  42066  brtrclfv2  42073  dfrtrcl3  42079  mnuprdlem1  42626  mnuprdlem2  42627  mullimc  43931  islptre  43934  mullimcf  43938  limcmptdm  43950  dvresntr  44233  itgperiod  44296  fourierdlem89  44510  fourierdlem91  44512  iccpartgt  45693  resmgmhm2  46167  setrecsres  47221
  Copyright terms: Public domain W3C validator