Theorem tpid1 4744

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {ctp 4605

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604  df-tp 4606

This theorem is referenced by:  tpnz  4755  hash3tpb  14513  wrdl3s3  14981  cffldtocusgr  29426  cffldtocusgrOLD  29427  umgrwwlks2on  29939  sgncl  32810  s3rnOLD  32921  cyc3evpm  33161  sgnsf  33173  prodfzo03  34635  circlevma  34674  circlemethhgt  34675  hgt750lemg  34686  hgt750lemb  34688  hgt750lema  34689  hgt750leme  34690  tgoldbachgtde  34692  tgoldbachgt  34695  kur14lem7  35234  kur14lem9  35236  brtpid1  35738  rabren3dioph  42838  fourierdlem102  46237  fourierdlem114  46249  etransclem48  46311  usgrexmpl1tri  48029  usgrexmpl2nb0  48035  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  gpg3kgrtriex  48091