Theorem eltp 4647

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

Syntax hints:   ↔ wb 206   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3441  {ctp 4585

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-sn 4582  df-pr 4584  df-tp 4586

This theorem is referenced by:  dftp2  4649  tpid1  4726  tpid2  4728  brtp  5472  tpres  7149  fntpb  7157  bpoly3  15985  cnfldfun  21327  cnfldfunOLD  21340  gausslemma2dlem0i  27335  2lgsoddprm  27387  sltsolem1  27647  nb3grprlem1  29436  frgr3vlem1  30331  frgr3vlem2  30332  prodtp  32889  s3f1  33010  hgt750lemb  34794  fmtno4prmfac  47854  usgrexmpl2nb0  48313  usgrexmpl2nb3  48316  usgrexmpl2trifr  48319  gpgnbgrvtx0  48356  gpgnbgrvtx1  48357