Theorem eltp 4643

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

Syntax hints:   ↔ wb 206   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3438  {ctp 4583

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582  df-tp 4584

This theorem is referenced by:  dftp2  4645  tpid1  4722  tpid2  4724  brtp  5470  tpres  7141  fntpb  7149  bpoly3  15983  cnfldfun  21293  cnfldfunOLD  21306  gausslemma2dlem0i  27291  2lgsoddprm  27343  sltsolem1  27603  nb3grprlem1  29343  frgr3vlem1  30235  frgr3vlem2  30236  prodtp  32785  s3f1  32901  hgt750lemb  34623  fmtno4prmfac  47557  usgrexmpl2nb0  48016  usgrexmpl2nb3  48019  usgrexmpl2trifr  48022  gpgnbgrvtx0  48059  gpgnbgrvtx1  48060