Theorem tpid1 4732

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

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  Vcvv 3453  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590  df-tp 4592

This theorem is used by:  tpnz  4743  hash3tpb  14564  s3rex  15025  wrdl3s3  15039  sgncl  15174  elcgrabasi  29262  cffldtocusgr  29915  usgrwwlks2on  30434  umgrwwlks2on  30435  cyc3evpm  33598  sgnsf  33610  prodfzo03  35119  circlevma  35158  circlemethhgt  35159  hgt750lemg  35170  hgt750lemb  35172  hgt750lema  35173  hgt750leme  35174  tgoldbachgtde  35176  tgoldbachgt  35179  kur14lem7  35799  kur14lem9  35801  brtpid1  36308  rabren3dioph  43664  fourierdlem102  47044  fourierdlem114  47056  etransclem48  47118  usgrexmpl1tri  48949  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  gpg3kgrtriex  49013