Theorem eltp 4660

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

Step	Hyp	Ref	Expression
1		eltp.1	. 2 ⊢ 𝐴 ∈ V
2		eltpg 4657	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  Vcvv 3458  {ctp 4598

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597  df-tp 4599

This theorem is used by:  dftp2  4662  tpid1  4739  tpid2  4741  brtp  5512  tpres  7206  fntpb  7214  bpoly3  16137  cnfldfun  21573  gausslemma2dlem0i  27565  2lgsoddprm  27617  ltssolem1  27876  nb3grprlem1  29767  frgr3vlem1  30661  frgr3vlem2  30662  prodtp  33208  s3f1  33301  hgt750lemb  35075  fmtno4prmfac  48365  usgrexmpl2nb0  48837  usgrexmpl2nb3  48840  usgrexmpl2trifr  48843  gpgnbgrvtx0  48880  gpgnbgrvtx1  48881