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

Theorem eltp 4654
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 4651 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3o 1087   = wceq 1542  wcel 2107  Vcvv 3448  {ctp 4595
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594  df-tp 4596
This theorem is referenced by:  dftp2  4655  tpid1  4734  tpid2  4736  brtp  5485  tpres  7155  fntpb  7164  bpoly3  15948  cnfldfun  20824  gausslemma2dlem0i  26728  2lgsoddprm  26780  sltsolem1  27039  nb3grprlem1  28370  frgr3vlem1  29259  frgr3vlem2  29260  prodtp  31765  s3f1  31845  hgt750lemb  33309  fmtno4prmfac  45838
  Copyright terms: Public domain W3C validator