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

Theorem tpeq123d 4038
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 4035 . 2  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  C ,  E } )
3 tpeq123d.2 . . 3  |-  ( ph  ->  C  =  D )
43tpeq2d 4036 . 2  |-  ( ph  ->  { B ,  C ,  E }  =  { B ,  D ,  E } )
5 tpeq123d.3 . . 3  |-  ( ph  ->  E  =  F )
65tpeq3d 4037 . 2  |-  ( ph  ->  { B ,  D ,  E }  =  { B ,  D ,  F } )
72, 4, 63eqtrd 2427 1  |-  ( ph  ->  { A ,  C ,  E }  =  { B ,  D ,  F } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   {ctp 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-sn 3945  df-pr 3947  df-tp 3949
This theorem is referenced by:  fz0tp  11699  fzo0to3tp  11799  prdsval  14862  imasval  14918  fucval  15364  fucpropd  15383  setcval  15473  catcval  15492  estrcval  15510  xpcval  15563  symgval  16521  psrval  18124  om1val  21615  usgraexvlem  24516  rabren3dioph  30914  mendval  31300  rngcvalALTV  32969  ringcvalALTV  33015  ldualset  35263  erngfset  36938  erngfset-rN  36946  dvafset  37143  dvaset  37144  dvhfset  37220  dvhset  37221  hlhilset  38077
  Copyright terms: Public domain W3C validator