Theorem eltp 4692

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

Syntax hints:   ↔ wb 205   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {ctp 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631  df-tp 4633

This theorem is referenced by:  dftp2  4693  tpid1  4772  tpid2  4774  brtp  5523  tpres  7201  fntpb  7210  bpoly3  16001  cnfldfun  20955  gausslemma2dlem0i  26864  2lgsoddprm  26916  sltsolem1  27175  nb3grprlem1  28634  frgr3vlem1  29523  frgr3vlem2  29524  prodtp  32028  s3f1  32108  hgt750lemb  33663  fmtno4prmfac  46230