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

Theorem eltp 4586
 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 4583 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {ctp 4529 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-tp 4530 This theorem is referenced by:  dftp2  4587  tpid1  4664  tpid2  4666  tpres  6940  fntpb  6949  bpoly3  15404  cnfldfunALT  20104  gausslemma2dlem0i  25948  2lgsoddprm  26000  nb3grprlem1  27170  frgr3vlem1  28058  frgr3vlem2  28059  prodtp  30569  s3f1  30649  hgt750lemb  32037  brtp  33098  sltsolem1  33293  fmtno4prmfac  44087
 Copyright terms: Public domain W3C validator