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

Theorem opeq2i 4597
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 4594 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2ax-mp 5 1 𝐶, 𝐴⟩ = ⟨𝐶, 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  cop 4374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375
This theorem is referenced by:  fnressn  6647  fressnfv  6649  wfrlem14  7662  seqomlem1  7779  recmulnq  10069  addresr  10242  seqval  13033  ids1  13590  wrdeqs1cat  13696  swrdccat3a  13716  ressinbas  16145  oduval  17333  mgmnsgrpex  17621  sgrpnmndex  17622  efgi0  18332  efgi1  18333  vrgpinv  18381  frgpnabllem1  18475  mat1dimid  20489  uspgr1v1eop  26355  clwlkclwwlkfo  27150  clwlksfoclwwlkOLD  27235  wlk2v2e  27328  avril1  27648  nvop  27857  phop  27999  signstfveq0  30977  bnj601  31311  tgrpset  36524  erngset  36579  erngset-rN  36587  pfx1  41984  pfxccatpfx2  42001  zlmodzxzadd  42702  lmod1  42847  lmod1zr  42848  zlmodzxzequa  42851  zlmodzxzequap  42854
  Copyright terms: Public domain W3C validator