Theorem tpid2 4739

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

Syntax hints:   ∨ w3o 1100   = wceq 1567   ∈ wcel 2149  Vcvv 3461  {ctp 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-un 3916  df-sn 4593  df-pr 4595  df-tp 4597

This theorem is referenced by:  1eltp012  12311  hash3tpb  14532  wrdl3s3  14999  sgncl  15134  wwlks2onv  30243  elwwlks2ons3im  30244  usgrwwlks2on  30248  umgrwwlks2on  30249  s3rnOLD  33207  cyc3evpm  33411  sgnsf  33423  signsw0glem  34885  signsw0g  34888  signswmnd  34889  signswrid  34890  prodfzo03  34935  circlevma  34974  circlemethhgt  34975  hgt750lemg  34986  hgt750lemb  34988  hgt750lema  34989  tgoldbachgtde  34992  tgoldbachgt  34995  kur14lem7  35637  brtpid2  36147  rabren3dioph  43469  oenord1ex  43969  oenord1  43970  fourierdlem102  46849  fourierdlem114  46861  etransclem48  46923  usgrexmpl1tri  48714  usgrexmpl2nb0  48720  usgrexmpl2nb1  48721  usgrexmpl2nb2  48722  usgrexmpl2nb3  48723  usgrexmpl2nb4  48724  usgrexmpl2nb5  48725