Theorem tpid1 4720

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 2733	. . 3 ⊢ 𝐴 = 𝐴
2	1	3mix1i 1334	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)
3		tpid1.1	. . 3 ⊢ 𝐴 ∈ V
4	3	eltp 4641	. 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	2, 4	mpbir 231	1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  Vcvv 3437  {ctp 4579

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578  df-tp 4580

This theorem is referenced by:  tpnz  4731  hash3tpb  14404  wrdl3s3  14871  cffldtocusgr  29427  cffldtocusgrOLD  29428  usgrwwlks2on  29938  umgrwwlks2on  29939  sgncl  32819  s3rnOLD  32934  cyc3evpm  33126  sgnsf  33138  prodfzo03  34637  circlevma  34676  circlemethhgt  34677  hgt750lemg  34688  hgt750lemb  34690  hgt750lema  34691  hgt750leme  34692  tgoldbachgtde  34694  tgoldbachgt  34697  kur14lem7  35277  kur14lem9  35279  brtpid1  35786  rabren3dioph  42933  fourierdlem102  46331  fourierdlem114  46343  etransclem48  46405  usgrexmpl1tri  48150  usgrexmpl2nb0  48156  usgrexmpl2nb1  48157  usgrexmpl2nb2  48158  usgrexmpl2nb3  48159  usgrexmpl2nb4  48160  usgrexmpl2nb5  48161  gpg3kgrtriex  48214