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

Theorem eltp 4693
Description: A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.)
Hypothesis
Ref Expression
eltp.1 𝐴 ∈ V
Assertion
Ref Expression
eltp (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))

Proof of Theorem eltp
StepHypRef Expression
1 eltp.1 . 2 𝐴 ∈ V
2 eltpg 4690 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3o 1087   = wceq 1542  wcel 2107  Vcvv 3475  {ctp 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632  df-tp 4634
This theorem is referenced by:  dftp2  4694  tpid1  4773  tpid2  4775  brtp  5524  tpres  7202  fntpb  7211  bpoly3  16002  cnfldfun  20956  gausslemma2dlem0i  26867  2lgsoddprm  26919  sltsolem1  27178  nb3grprlem1  28637  frgr3vlem1  29526  frgr3vlem2  29527  prodtp  32033  s3f1  32113  hgt750lemb  33668  fmtno4prmfac  46240
  Copyright terms: Public domain W3C validator