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

Theorem opeq2i 4876
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
opeq2i 𝐶, 𝐴⟩ = ⟨𝐶, 𝐵

Proof of Theorem opeq2i
StepHypRef Expression
1 opeq1i.1 . 2 𝐴 = 𝐵
2 opeq2 4873 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2ax-mp 5 1 𝐶, 𝐴⟩ = ⟨𝐶, 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  cop 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634
This theorem is referenced by:  fnressn  7152  fressnfv  7154  wfrlem14OLD  8318  seqomlem1  8446  recmulnq  10955  addresr  11129  seqval  13973  ids1  14543  pfx1  14649  pfxccatpfx2  14683  ressinbas  17186  oduval  18237  mgmnsgrpex  18808  sgrpnmndex  18809  efgi0  19582  efgi1  19583  vrgpinv  19631  frgpnabllem1  19735  mat1dimid  21967  uspgr1v1eop  28495  wlk2v2e  29399  avril1  29705  nvop  29916  phop  30058  bnj601  33919  tgrpset  39604  erngset  39659  erngset-rN  39667  zlmodzxzadd  46987  lmod1  47126  lmod1zr  47127  zlmodzxzequa  47130  zlmodzxzequap  47133
  Copyright terms: Public domain W3C validator