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

Theorem eqsstrrd 4009
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 2831 . 2 (𝜑𝐴 = 𝐵)
3 eqsstrrd.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrd 4008 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  ssxpb  6028  fnsnr  6922  suppssof1  7857  oaword1  8171  omword2  8193  oeeui  8221  nnaword1  8248  cantnfle  9126  cantnflem1d  9143  r1val1  9207  rankr1id  9283  rankxplim3  9302  ackbij2  9657  ttukeylem7  9929  gruima  10216  hashdmpropge2  13834  rlimi  14863  rlimi2  14864  lo1bdd  14870  o1bdd  14881  rlimuni  14900  rlimcld2  14928  o1co  14936  rlimcn1  14938  rlimcn2  14940  o1add2  14973  o1mul2  14974  o1sub2  14975  lo1add  14976  lo1mul  14977  o1dif  14979  rlimneg  14996  rlimsqzlem  14998  lo1le  15001  rlimno1  15003  ramub1lem1  16354  imasaddfnlem  16793  imasvscafn  16802  mrcidb  16878  mrieqv2d  16902  mreexexlem4d  16910  funcres  17158  funcsetcres2  17345  acsfiindd  17779  tsrdir  17840  resmhm2  17971  f1omvdco2  18498  sylow2a  18666  sylow3lem6  18679  dprdspan  19071  dprd2dlem2  19084  dprd2dlem1  19085  dprd2da  19086  dmdprdsplit2lem  19089  dprdsplit  19092  dpjcntz  19096  ablfac1eu  19117  ringidss  19249  subrg1  19467  subrgdvds  19471  subrguss  19472  subrginv  19473  subdrgint  19504  primefld  19506  islss3  19653  lspsnneg  19700  lspextmo  19750  lspsnvs  19808  lsmcv  19835  islbs3  19849  drngdomn  19997  psrbaglesupp  20069  resspsrbas  20116  resspsradd  20117  resspsrmul  20118  evlseu  20216  f1lindf  20882  epttop  21533  neitr  21704  ordtbas  21716  ordtrest2  21728  pnfnei  21744  mnfnei  21745  ordtrestixx  21746  dnsconst  21902  cmpcld  21926  txindis  22158  txtube  22164  xkohaus  22177  xkopt  22179  xkococnlem  22183  xkoinjcn  22211  qtopval2  22220  ssufl  22442  ufldom  22486  cnextcn  22591  tmdgsum2  22620  clssubg  22632  clsnsg  22633  ustund  22745  ustneism  22747  trust  22753  fmucnd  22816  imasdsf1olem  22898  setsmstopn  23003  metequiv2  23035  metust  23083  restmetu  23095  tngtopn  23174  xlebnum  23484  pi1xfrcnv  23576  limcdif  24389  limccnp  24404  limccnp2  24405  limcco  24406  dvn2bss  24442  cpnord  24447  dvcmulf  24457  dvmptres2  24474  dvmptcmul  24476  dvmptntr  24483  dvcnvrelem2  24530  dvcnvre  24531  taylthlem1  24876  taylthlem2  24877  ulmdvlem3  24905  psercnlem2  24927  rlimcxp  25465  o1cxp  25466  sspg  28419  ssps  28421  sspn  28427  mdslj1i  30010  mdslj2i  30011  sh1dle  30042  shatomistici  30052  sumdmdii  30106  unidifsnel  30209  resf1o  30379  symgcom2  30642  submarchi  30729  fedgmullem1  30911  fedgmullem2  30912  fedgmul  30913  extdg1id  30939  madjusmdetlem1  30978  txomap  30984  cnvordtrestixx  31042  dya2iocucvr  31428  carsggect  31462  bnj1241  31965  bnj906  32088  cvmscld  32404  nosupbnd2lem1  33099  noetalem4  33104  fvline2  33491  cldregopn  33563  pibt2  34567  poimirlem15  34774  sstotbnd2  34920  totbndbnd  34935  heibor1  34956  heiborlem8  34964  lsmsat  36011  lssats  36015  lkrpssN  36166  dia2dimlem5  38071  cdlemn2a  38199  dihglblem6  38343  dochocsp  38382  dochdmj1  38393  dochsatshpb  38455  lcfl9a  38508  lclkrlem2r  38527  lclkrlem2s  38528  lclkrlem2v  38531  lcfrlem6  38550  lcfrlem25  38570  lcfrlem35  38580  mapdval2N  38633  mapdin  38665  baerlem5alem2  38714  baerlem5blem2  38715  dnnumch2  39506  clrellem  39843  iunrelexpmin1  39914  iunrelexpmin2  39918  dftrcl3  39926  brtrclfv2  39933  dfrtrcl3  39939  mnuprdlem1  40469  mnuprdlem2  40470  mullimc  41758  islptre  41761  mullimcf  41765  limcmptdm  41777  dvresntr  42063  itgperiod  42127  fourierdlem89  42342  fourierdlem91  42344  iccpartgt  43415  resmgmhm2  43894  setrecsres  44632
  Copyright terms: Public domain W3C validator