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

Theorem tpeq123d 4773
Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
Hypotheses
Ref Expression
tpeq1d.1 (𝜑𝐴 = 𝐵)
tpeq123d.2 (𝜑𝐶 = 𝐷)
tpeq123d.3 (𝜑𝐸 = 𝐹)
Assertion
Ref Expression
tpeq123d (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})

Proof of Theorem tpeq123d
StepHypRef Expression
1 tpeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21tpeq1d 4770 . 2 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸})
3 tpeq123d.2 . . 3 (𝜑𝐶 = 𝐷)
43tpeq2d 4771 . 2 (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸})
5 tpeq123d.3 . . 3 (𝜑𝐸 = 𝐹)
65tpeq3d 4772 . 2 (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹})
72, 4, 63eqtrd 2784 1 (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  {ctp 4652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651  df-tp 4653
This theorem is referenced by:  fz0tp  13685  fz0to5un2tp  13688  fzo0to3tp  13802  fzo1to4tp  13804  prdsval  17515  imasval  17571  fucval  18027  fucpropd  18047  setcval  18144  catcval  18167  estrcval  18192  xpcval  18246  efmnd  18905  dfcnfldOLD  21403  psrval  21958  om1val  25082  s3rnOLD  32912  rlocval  33231  idlsrgval  33496  ldualset  39081  erngfset  40756  erngfset-rN  40764  dvafset  40961  dvaset  40962  dvhfset  41037  dvhset  41038  hlhilset  41891  rabren3dioph  42771  mendval  43140  oaun3  43344  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  rngcvalALTV  47988  ringcvalALTV  48012  mndtcval  48752
  Copyright terms: Public domain W3C validator