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

Theorem eltp 4533
 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 4530 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∨ w3o 1079   = wceq 1522   ∈ wcel 2081  Vcvv 3437  {ctp 4476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3864  df-sn 4473  df-pr 4475  df-tp 4477 This theorem is referenced by:  dftp2  4534  tpid1  4611  tpid2  4613  tpres  6830  fntpb  6838  bpoly3  15245  cnfldfunALT  20240  gausslemma2dlem0i  25622  2lgsoddprm  25674  nb3grprlem1  26845  frgr3vlem1  27744  frgr3vlem2  27745  prodtp  30227  s3f1  30303  hgt750lemb  31544  brtp  32593  sltsolem1  32789  fmtno4prmfac  43216
 Copyright terms: Public domain W3C validator