Theorem tpid1 4727

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

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {ctp 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585  df-tp 4587

This theorem is referenced by:  tpnz  4738  hash3tpb  14430  wrdl3s3  14897  cffldtocusgr  29532  cffldtocusgrOLD  29533  usgrwwlks2on  30043  umgrwwlks2on  30044  sgncl  32922  s3rnOLD  33038  cyc3evpm  33243  sgnsf  33255  prodfzo03  34780  circlevma  34819  circlemethhgt  34820  hgt750lemg  34831  hgt750lemb  34833  hgt750lema  34834  hgt750leme  34835  tgoldbachgtde  34837  tgoldbachgt  34840  kur14lem7  35425  kur14lem9  35427  brtpid1  35934  rabren3dioph  43166  fourierdlem102  46560  fourierdlem114  46572  etransclem48  46634  usgrexmpl1tri  48379  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  gpg3kgrtriex  48443