Theorem tpid1 4706

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

Syntax hints:   ∨ w3o 1082   = wceq 1537   ∈ wcel 2114  Vcvv 3496  {ctp 4573

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-pr 4572  df-tp 4574

This theorem is referenced by:  tpnz  4716  wrdl3s3  14328  cffldtocusgr  27231  umgrwwlks2on  27738  s3rn  30624  cyc3evpm  30794  sgnsf  30806  sgncl  31798  prodfzo03  31876  circlevma  31915  circlemethhgt  31916  hgt750lemg  31927  hgt750lemb  31929  hgt750lema  31930  hgt750leme  31931  tgoldbachgtde  31933  tgoldbachgt  31936  kur14lem7  32461  kur14lem9  32463  brtpid1  32953  rabren3dioph  39419  fourierdlem102  42500  fourierdlem114  42512  etransclem48  42574