Theorem tpid2 4776

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 2736	. . 3 ⊢ 𝐵 = 𝐵
2	1	3mix2i 1334	. 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)
3		tpid2.1	. . 3 ⊢ 𝐵 ∈ V
4	3	eltp 4695	. 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))
5	2, 4	mpbir 231	1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1085   = wceq 1538   ∈ wcel 2107  Vcvv 3479  {ctp 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1541  df-ex 1778  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3969  df-sn 4633  df-pr 4635  df-tp 4637

This theorem is referenced by:  hash3tpb  14537  wrdl3s3  15004  wwlks2onv  29996  elwwlks2ons3im  29997  umgrwwlks2on  30000  s3rnOLD  32928  cyc3evpm  33166  sgnsf  33178  sgncl  34533  signsw0glem  34560  signsw0g  34563  signswmnd  34564  signswrid  34565  prodfzo03  34610  circlevma  34649  circlemethhgt  34650  hgt750lemg  34661  hgt750lemb  34663  hgt750lema  34664  hgt750leme  34665  tgoldbachgtde  34667  tgoldbachgt  34670  kur14lem7  35209  brtpid2  35714  rabren3dioph  42817  oenord1ex  43319  oenord1  43320  fourierdlem102  46175  fourierdlem114  46187  etransclem48  46249  usgrexmpl1tri  47933  usgrexmpl2nb0  47939  usgrexmpl2nb1  47940  usgrexmpl2nb2  47941  usgrexmpl2nb3  47942  usgrexmpl2nb4  47943  usgrexmpl2nb5  47944