Theorem eltp 4694

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

Syntax hints:   ↔ wb 206   ∨ w3o 1085   = wceq 1537   ∈ wcel 2106  Vcvv 3478  {ctp 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634  df-tp 4636

This theorem is referenced by:  dftp2  4696  tpid1  4773  tpid2  4775  brtp  5533  tpres  7221  fntpb  7229  bpoly3  16091  cnfldfun  21396  cnfldfunOLD  21409  gausslemma2dlem0i  27423  2lgsoddprm  27475  sltsolem1  27735  nb3grprlem1  29412  frgr3vlem1  30302  frgr3vlem2  30303  prodtp  32834  s3f1  32916  hgt750lemb  34650  fmtno4prmfac  47497  usgrexmpl2nb0  47926  usgrexmpl2nb3  47929  usgrexmpl2trifr  47932  gpgnbgrvtx0  47965  gpgnbgrvtx1  47966