Theorem tpid2 4725

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

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {ctp 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581  df-tp 4583

This theorem is referenced by:  hash3tpb  14416  wrdl3s3  14883  wwlks2onv  29975  elwwlks2ons3im  29976  usgrwwlks2on  29980  umgrwwlks2on  29981  sgncl  32861  s3rnOLD  32977  cyc3evpm  33181  sgnsf  33193  signsw0glem  34659  signsw0g  34662  signswmnd  34663  signswrid  34664  prodfzo03  34709  circlevma  34748  circlemethhgt  34749  hgt750lemg  34760  hgt750lemb  34762  hgt750lema  34763  hgt750leme  34764  tgoldbachgtde  34766  tgoldbachgt  34769  kur14lem7  35355  brtpid2  35865  rabren3dioph  42999  oenord1ex  43499  oenord1  43500  fourierdlem102  46394  fourierdlem114  46406  etransclem48  46468  usgrexmpl1tri  48213  usgrexmpl2nb0  48219  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224