Theorem tpid1 4732

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {ctp 4593

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592  df-tp 4594

This theorem is referenced by:  tpnz  4743  hash3tpb  14460  wrdl3s3  14928  cffldtocusgr  29374  cffldtocusgrOLD  29375  umgrwwlks2on  29887  sgncl  32756  s3rnOLD  32867  cyc3evpm  33107  sgnsf  33119  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  kur14lem7  35199  kur14lem9  35201  brtpid1  35708  rabren3dioph  42803  fourierdlem102  46206  fourierdlem114  46218  etransclem48  46280  usgrexmpl1tri  48016  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpg3kgrtriex  48080