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

Theorem opeq1i 4805
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 4802 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2ax-mp 5 1 𝐴, 𝐶⟩ = ⟨𝐵, 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  cop 4572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573
This theorem is referenced by:  axi2m1  10580  s3tpop  14270  2strstr1  16604  2strop1  16606  grpbasex  16612  grpplusgx  16613  mat1dimelbas  21079  mat1dim0  21081  mat1dimid  21082  mat1dimscm  21083  mat1dimmul  21084  indistpsx  21617  setsiedg  26820  cusgrsize  27235  mapfzcons  39311
  Copyright terms: Public domain W3C validator