Theorem tpid2 4752

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

Syntax hints:   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  Vcvv 3464  {ctp 4612

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-sn 4609  df-pr 4611  df-tp 4613

This theorem is referenced by:  hash3tpb  14517  wrdl3s3  14984  wwlks2onv  29920  elwwlks2ons3im  29921  umgrwwlks2on  29924  s3rnOLD  32877  cyc3evpm  33116  sgnsf  33128  sgncl  34482  signsw0glem  34509  signsw0g  34512  signswmnd  34513  signswrid  34514  prodfzo03  34559  circlevma  34598  circlemethhgt  34599  hgt750lemg  34610  hgt750lemb  34612  hgt750lema  34613  hgt750leme  34614  tgoldbachgtde  34616  tgoldbachgt  34619  kur14lem7  35158  brtpid2  35663  rabren3dioph  42771  oenord1ex  43273  oenord1  43274  fourierdlem102  46168  fourierdlem114  46180  etransclem48  46242  usgrexmpl1tri  47930  usgrexmpl2nb0  47936  usgrexmpl2nb1  47937  usgrexmpl2nb2  47938  usgrexmpl2nb3  47939  usgrexmpl2nb4  47940  usgrexmpl2nb5  47941