Theorem tpid1 4726

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

Syntax hints:   ∨ w3o 1096   = wceq 1559   ∈ wcel 2141  Vcvv 3453  {ctp 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4582  df-pr 4584  df-tp 4586

This theorem is referenced by:  tpnz  4737  hash3tpb  14505  wrdl3s3  14972  cffldtocusgr  29594  usgrwwlks2on  30104  umgrwwlks2on  30105  sgncl  32983  s3rnOLD  33085  cyc3evpm  33291  sgnsf  33303  prodfzo03  34861  circlevma  34900  circlemethhgt  34901  hgt750lemg  34912  hgt750lemb  34914  hgt750lema  34915  hgt750leme  34916  tgoldbachgtde  34918  tgoldbachgt  34921  kur14lem7  35526  kur14lem9  35528  brtpid1  36035  rabren3dioph  43356  fourierdlem102  46746  fourierdlem114  46758  etransclem48  46820  usgrexmpl1tri  48611  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  gpg3kgrtriex  48675