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

Theorem oteq3 4167
Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
oteq3  |-  ( A  =  B  ->  <. C ,  D ,  A >.  = 
<. C ,  D ,  B >. )

Proof of Theorem oteq3
StepHypRef Expression
1 opeq2 4157 . 2  |-  ( A  =  B  ->  <. <. C ,  D >. ,  A >.  = 
<. <. C ,  D >. ,  B >. )
2 df-ot 3978 . 2  |-  <. C ,  D ,  A >.  = 
<. <. C ,  D >. ,  A >.
3 df-ot 3978 . 2  |-  <. C ,  D ,  B >.  = 
<. <. C ,  D >. ,  B >.
41, 2, 33eqtr4g 2466 1  |-  ( A  =  B  ->  <. C ,  D ,  A >.  = 
<. C ,  D ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1403   <.cop 3975   <.cotp 3977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-rab 2760  df-v 3058  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-sn 3970  df-pr 3972  df-op 3976  df-ot 3978
This theorem is referenced by:  oteq3d  4170  otsndisj  4692  otiunsndisj  4693  efgi0  16952  efgi1  16953  mapdhcl  34711  mapdh6dN  34723  mapdh8  34773  mapdh9a  34774  mapdh9aOLDN  34775  hdmap1l6d  34798  hdmapval  34815  hdmapval2  34819  hdmapval3N  34825  otiunsndisjX  37866
  Copyright terms: Public domain W3C validator