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

Theorem tpeq123d 4109
Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
Hypotheses
Ref Expression
tpeq1d.1  |-  ( ph  ->  A  =  B )
tpeq123d.2  |-  ( ph  ->  C  =  D )
tpeq123d.3  |-  ( ph  ->  E  =  F )
Assertion
Ref Expression
tpeq123d  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  D ,  F } )

Proof of Theorem tpeq123d
StepHypRef Expression
1 tpeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21tpeq1d 4106 . 2  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  C ,  E } )
3 tpeq123d.2 . . 3  |-  ( ph  ->  C  =  D )
43tpeq2d 4107 . 2  |-  ( ph  ->  { B ,  C ,  E }  =  { B ,  D ,  E } )
5 tpeq123d.3 . . 3  |-  ( ph  ->  E  =  F )
65tpeq3d 4108 . 2  |-  ( ph  ->  { B ,  D ,  E }  =  { B ,  D ,  F } )
72, 4, 63eqtrd 2488 1  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  D ,  F } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   {ctp 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017  df-tp 4019
This theorem is referenced by:  fz0tp  11785  fzo0to3tp  11879  prdsval  14729  imasval  14785  fucval  15201  fucpropd  15220  setcval  15278  catcval  15297  xpcval  15320  symgval  16278  psrval  17885  om1val  21403  usgraexvlem  24267  rabren3dioph  30724  mendval  31108  estrcval  32479  rngcvalOLD  32509  ringcvalOLD  32552  ldualset  34590  erngfset  36265  erngfset-rN  36273  dvafset  36470  dvaset  36471  dvhfset  36547  dvhset  36548  hlhilset  37404
  Copyright terms: Public domain W3C validator