Theorem tpid2 4727

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

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {ctp 4584

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583  df-tp 4585

This theorem is referenced by:  hash3tpb  14420  wrdl3s3  14887  wwlks2onv  30028  elwwlks2ons3im  30029  usgrwwlks2on  30033  umgrwwlks2on  30034  sgncl  32914  s3rnOLD  33030  cyc3evpm  33234  sgnsf  33246  signsw0glem  34712  signsw0g  34715  signswmnd  34716  signswrid  34717  prodfzo03  34762  circlevma  34801  circlemethhgt  34802  hgt750lemg  34813  hgt750lemb  34815  hgt750lema  34816  hgt750leme  34817  tgoldbachgtde  34819  tgoldbachgt  34822  kur14lem7  35408  brtpid2  35918  rabren3dioph  43078  oenord1ex  43578  oenord1  43579  fourierdlem102  46473  fourierdlem114  46485  etransclem48  46547  usgrexmpl1tri  48292  usgrexmpl2nb0  48298  usgrexmpl2nb1  48299  usgrexmpl2nb2  48300  usgrexmpl2nb3  48301  usgrexmpl2nb4  48302  usgrexmpl2nb5  48303