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

Theorem eltp 4177
 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 4174 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {ctp 4129 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128  df-tp 4130 This theorem is referenced by:  dftp2  4178  tpid1  4246  tpid2  4247  tpres  6371  fntpb  6378  bpoly3  14628  gausslemma2dlem0i  24889  2lgsoddprm  24941  nb3graprlem1  25980  frgra3vlem1  26527  frgra3vlem2  26528  brtp  30892  sltsolem1  31067  fmtno4prmfac  40022  nb3grprlem1  40608  frgr3vlem1  41443  frgr3vlem2  41444
 Copyright terms: Public domain W3C validator