Theorem eltp 4656

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 4653	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

Syntax hints:   ↔ wb 209   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {ctp 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593  df-tp 4595

This theorem is referenced by:  dftp2  4658  tpid1  4735  tpid2  4737  brtp  5509  tpres  7201  fntpb  7209  bpoly3  16113  cnfldfun  21517  gausslemma2dlem0i  27506  2lgsoddprm  27558  ltssolem1  27817  nb3grprlem1  29708  frgr3vlem1  30602  frgr3vlem2  30603  prodtp  33149  s3f1  33245  hgt750lemb  35021  fmtno4prmfac  48301  usgrexmpl2nb0  48773  usgrexmpl2nb3  48776  usgrexmpl2trifr  48779  gpgnbgrvtx0  48816  gpgnbgrvtx1  48817