Theorem tpid1 4735

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

Syntax hints:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {ctp 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593  df-tp 4595

This theorem is referenced by:  tpnz  4746  hash3tpb  14534  wrdl3s3  15001  sgncl  15136  cffldtocusgr  29775  usgrwwlks2on  30285  umgrwwlks2on  30286  s3rnOLD  33244  cyc3evpm  33448  sgnsf  33460  prodfzo03  34968  circlevma  35007  circlemethhgt  35008  hgt750lemg  35019  hgt750lemb  35021  hgt750lema  35022  hgt750leme  35023  tgoldbachgtde  35025  tgoldbachgt  35028  kur14lem7  35682  kur14lem9  35684  brtpid1  36191  rabren3dioph  43522  fourierdlem102  46902  fourierdlem114  46914  etransclem48  46976  usgrexmpl1tri  48767  usgrexmpl2nb0  48773  usgrexmpl2nb1  48774  usgrexmpl2nb2  48775  usgrexmpl2nb3  48776  usgrexmpl2nb4  48777  usgrexmpl2nb5  48778  gpg3kgrtriex  48831