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

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

Proof of Theorem opeq1i
StepHypRef Expression
1 opeq1i.1 . 2 𝐴 = 𝐵
2 opeq1 4759 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2ax-mp 5 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cop 4522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-sn 4517  df-pr 4519  df-op 4523
This theorem is referenced by:  axi2m1  10661  s3tpop  14362  2strstr1  16710  2strop1  16712  grpbasex  16718  grpplusgx  16719  mat1dimelbas  21224  mat1dim0  21226  mat1dimid  21227  mat1dimscm  21228  mat1dimmul  21229  indistpsx  21763  setsiedg  26983  cusgrsize  27398  nosupcbv  33550  noinfcbv  33565  mapfzcons  40132
  Copyright terms: Public domain W3C validator