Theorem tpid1 4704

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

Syntax hints:   ∨ w3o 1085   = wceq 1539   ∈ wcel 2106  Vcvv 3432  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564  df-tp 4566

This theorem is referenced by:  tpnz  4715  wrdl3s3  14677  cffldtocusgr  27814  umgrwwlks2on  28322  s3rn  31220  cyc3evpm  31417  sgnsf  31429  sgncl  32505  prodfzo03  32583  circlevma  32622  circlemethhgt  32623  hgt750lemg  32634  hgt750lemb  32636  hgt750lema  32637  hgt750leme  32638  tgoldbachgtde  32640  tgoldbachgt  32643  kur14lem7  33174  kur14lem9  33176  brtpid1  33665  rabren3dioph  40637  fourierdlem102  43749  fourierdlem114  43761  etransclem48  43823