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

Theorem opeq2i 3800
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1i.1  |-  A  =  B
Assertion
Ref Expression
opeq2i  |-  <. C ,  A >.  =  <. C ,  B >.

Proof of Theorem opeq2i
StepHypRef Expression
1 opeq1i.1 . 2  |-  A  =  B
2 opeq2 3797 . 2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
31, 2ax-mp 8 1  |-  <. C ,  A >.  =  <. C ,  B >.
Colors of variables: wff set class
Syntax hints:    = wceq 1623   <.cop 3643
This theorem is referenced by:  fnressn  5705  fressnfv  5707  seqomlem1  6462  recmulnq  8588  addresr  8760  seqval  11057  ids1  11437  wrdeqs1cat  11475  ressinbas  13204  oduval  14234  efgi0  15029  efgi1  15030  vrgpinv  15078  frgpnabllem1  15161  zlmval  16470  avril1  20836  ginvsn  21016  nvop  21243  phop  21396  orrvcval4  23665  orrvcoel  23666  orrvccel  23667  vdgr1c  23896  wfrlem14  24269  bnj601  28952  tgrpset  30934  erngset  30989  erngset-rN  30997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator