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

Theorem oteq3 3823
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 3813 . 2  |-  ( A  =  B  ->  <. <. C ,  D >. ,  A >.  = 
<. <. C ,  D >. ,  B >. )
2 df-ot 3663 . 2  |-  <. C ,  D ,  A >.  = 
<. <. C ,  D >. ,  A >.
3 df-ot 3663 . 2  |-  <. C ,  D ,  B >.  = 
<. <. C ,  D >. ,  B >.
41, 2, 33eqtr4g 2353 1  |-  ( A  =  B  ->  <. C ,  D ,  A >.  = 
<. C ,  D ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   <.cop 3656   <.cotp 3657
This theorem is referenced by:  oteq3d  3826  efgi  15044  efgi0  15045  efgi1  15046  efgtf  15047  efgtval  15048  efgval2  15049  mapdhcl  32539  mapdh6bN  32549  mapdh6cN  32550  mapdh6dN  32551  mapdh6gN  32554  mapdh8  32601  mapdh9a  32602  mapdh9aOLDN  32603  hdmap1l6b  32624  hdmap1l6c  32625  hdmap1l6d  32626  hdmap1l6g  32629  hdmapval  32643  hdmapval2  32647  hdmapval3N  32653
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-ot 3663
  Copyright terms: Public domain W3C validator