Theorem eltpi 4652

Description: A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)

Assertion

Ref	Expression
eltpi	⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

Proof of Theorem eltpi

Step	Hyp	Ref	Expression
1		eltpg 4650	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
2	1	ibi 270	1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590  df-tp 4592

This theorem is used by:  fvf1tp  13854  tpfo  14569  sgnmulsgn  15186  prm23lt5  16912  perfectlem2  27474  zabsle1  27540  sgnmulsgp  33310  gsumtp  33512  cyc3co2  33588  kur14lem7  35799  omcl3g  44183  fmtnofz04prm  48488  perfectALTVlem2  48646  gpgprismgr4cycllem7  49025  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem6  49048  crosspaltd  50807  crossp3d  50808