Theorem tpid2 4731

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
tpid2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
tpid2	⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid2

Step	Hyp	Ref	Expression
1		eqid 2764	. . 3 ⊢ 𝐵 = 𝐵
2	1	3mix2i 1349	. 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)
3		tpid2.1	. . 3 ⊢ 𝐵 ∈ V
4	3	eltp 4650	. 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))
5	2, 4	mpbir 233	1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1098   = wceq 1562   ∈ wcel 2144  Vcvv 3456  {ctp 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-un 3911  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is referenced by:  1eltp012  12290  hash3tpb  14510  wrdl3s3  14977  sgncl  15112  wwlks2onv  30155  elwwlks2ons3im  30156  usgrwwlks2on  30160  umgrwwlks2on  30161  s3rnOLD  33126  cyc3evpm  33332  sgnsf  33344  signsw0glem  34849  signsw0g  34852  signswmnd  34853  signswrid  34854  prodfzo03  34899  circlevma  34938  circlemethhgt  34939  hgt750lemg  34950  hgt750lemb  34952  hgt750lema  34953  tgoldbachgtde  34956  tgoldbachgt  34959  kur14lem7  35567  brtpid2  36077  rabren3dioph  43397  oenord1ex  43897  oenord1  43898  fourierdlem102  46787  fourierdlem114  46799  etransclem48  46861  usgrexmpl1tri  48652  usgrexmpl2nb0  48658  usgrexmpl2nb1  48659  usgrexmpl2nb2  48660  usgrexmpl2nb3  48661  usgrexmpl2nb4  48662  usgrexmpl2nb5  48663