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 206   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {ctp 4596

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595  df-tp 4597

This theorem is referenced by:  dftp2  4658  tpid1  4735  tpid2  4737  brtp  5486  tpres  7178  fntpb  7186  bpoly3  16031  cnfldfun  21285  cnfldfunOLD  21298  gausslemma2dlem0i  27282  2lgsoddprm  27334  sltsolem1  27594  nb3grprlem1  29314  frgr3vlem1  30209  frgr3vlem2  30210  prodtp  32759  s3f1  32875  hgt750lemb  34654  fmtno4prmfac  47577  usgrexmpl2nb0  48026  usgrexmpl2nb3  48029  usgrexmpl2trifr  48032  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070