Theorem tpid1 4725

Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Hypothesis

Ref	Expression
tpid1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
tpid1	⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid1

Step	Hyp	Ref	Expression
1		eqid 2736	. . 3 ⊢ 𝐴 = 𝐴
2	1	3mix1i 1334	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)
3		tpid1.1	. . 3 ⊢ 𝐴 ∈ V
4	3	eltp 4646	. 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	2, 4	mpbir 231	1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {ctp 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583  df-tp 4585

This theorem is referenced by:  tpnz  4736  hash3tpb  14418  wrdl3s3  14885  cffldtocusgr  29520  cffldtocusgrOLD  29521  usgrwwlks2on  30031  umgrwwlks2on  30032  sgncl  32912  s3rnOLD  33028  cyc3evpm  33232  sgnsf  33244  prodfzo03  34760  circlevma  34799  circlemethhgt  34800  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgt  34820  kur14lem7  35406  kur14lem9  35408  brtpid1  35915  rabren3dioph  43053  fourierdlem102  46448  fourierdlem114  46460  etransclem48  46522  usgrexmpl1tri  48267  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2nb4  48277  usgrexmpl2nb5  48278  gpg3kgrtriex  48331