Theorem tpid1 4722

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 4643	. 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	2, 4	mpbir 231	1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3438  {ctp 4583

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 3440  df-un 3910  df-sn 4580  df-pr 4582  df-tp 4584

This theorem is referenced by:  tpnz  4733  hash3tpb  14420  wrdl3s3  14887  cffldtocusgr  29410  cffldtocusgrOLD  29411  umgrwwlks2on  29920  sgncl  32789  s3rnOLD  32900  cyc3evpm  33105  sgnsf  33117  prodfzo03  34570  circlevma  34609  circlemethhgt  34610  hgt750lemg  34621  hgt750lemb  34623  hgt750lema  34624  hgt750leme  34625  tgoldbachgtde  34627  tgoldbachgt  34630  kur14lem7  35184  kur14lem9  35186  brtpid1  35693  rabren3dioph  42788  fourierdlem102  46190  fourierdlem114  46202  etransclem48  46264  usgrexmpl1tri  48010  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  gpg3kgrtriex  48074