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

Theorem eltp 4689
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 4686 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷)))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵𝐴 = 𝐶𝐴 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wb 206  w3o 1086   = wceq 1540  wcel 2108  Vcvv 3480  {ctp 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629  df-tp 4631
This theorem is referenced by:  dftp2  4691  tpid1  4768  tpid2  4770  brtp  5528  tpres  7221  fntpb  7229  bpoly3  16094  cnfldfun  21378  cnfldfunOLD  21391  gausslemma2dlem0i  27408  2lgsoddprm  27460  sltsolem1  27720  nb3grprlem1  29397  frgr3vlem1  30292  frgr3vlem2  30293  prodtp  32829  s3f1  32931  hgt750lemb  34671  fmtno4prmfac  47559  usgrexmpl2nb0  47990  usgrexmpl2nb3  47993  usgrexmpl2trifr  47996  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031
  Copyright terms: Public domain W3C validator