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

Theorem eleqtrrid 2922
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eleqtrrid.1 𝐴𝐵
eleqtrrid.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
eleqtrrid (𝜑𝐴𝐶)

Proof of Theorem eleqtrrid
StepHypRef Expression
1 eleqtrrid.1 . 2 𝐴𝐵
2 eleqtrrid.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2829 . 2 (𝜑𝐵 = 𝐶)
41, 3eleqtrid 2921 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895
This theorem is referenced by:  rabsnt  4669  onnev  6313  opabiota  6748  canth  7113  onnseq  7983  tfrlem16  8031  oen0  8214  nnawordex  8265  inf0  9086  cantnflt  9137  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  r1ordg  9209  r1val1  9217  rankr1id  9293  acacni  9568  dfacacn  9569  dfac13  9570  ttukeylem5  9937  ttukeylem6  9938  gch2  10099  gch3  10100  gchac  10105  gchina  10123  swrds1  14030  wrdl3s3  14328  sadcp1  15806  lcmfunsnlem2  15986  fnpr2ob  16833  idfucl  17153  gsumval2  17898  gsumz  18002  frmdmnd  18026  frmd0  18027  efginvrel2  18855  efgcpbl2  18885  pgpfaclem1  19205  lbsexg  19938  zringndrg  20639  frlmlbs  20943  mat0dimscm  21080  mat0scmat  21149  m2detleiblem5  21236  m2detleiblem6  21237  m2detleiblem3  21240  m2detleiblem4  21241  d0mat2pmat  21348  chpmat0d  21444  dfac14  22228  acufl  22527  cnextfvval  22675  cnextcn  22677  minveclem3b  24033  minveclem4a  24035  ovollb2  24092  ovolunlem1a  24099  ovolunlem1  24100  ovoliunlem1  24105  ovoliun2  24109  ioombl1lem4  24164  uniioombllem1  24184  uniioombllem2  24186  uniioombllem6  24191  itg2monolem1  24353  itg2mono  24356  itg2cnlem1  24364  xrlimcnp  25548  efrlim  25549  eengbas  26769  ebtwntg  26770  ecgrtg  26771  elntg  26772  wlkl1loop  27421  elwwlks2ons3im  27735  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  2clwwlk2clwwlk  28131  ex-br  28212  trsp2cyc  30767  cyc3evpm  30794  lvecdim0  31007  extdg1id  31055  rge0scvg  31194  repr0  31884  hgt750lemg  31927  mrsub0  32765  elmrsubrn  32769  topjoin  33715  finorwe  34665  pclfinN  37038  aomclem1  39661  dfac21  39673  clsk1indlem1  40402  mnurndlem1  40624  fourierdlem102  42500  fourierdlem114  42512  lincval0  44477  lcoel0  44490
  Copyright terms: Public domain W3C validator