Theorem tpid2 4729

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

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {ctp 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585  df-tp 4587

This theorem is referenced by:  hash3tpb  14430  wrdl3s3  14897  wwlks2onv  30042  elwwlks2ons3im  30043  usgrwwlks2on  30047  umgrwwlks2on  30048  sgncl  32927  s3rnOLD  33043  cyc3evpm  33248  sgnsf  33260  signsw0glem  34735  signsw0g  34738  signswmnd  34739  signswrid  34740  prodfzo03  34785  circlevma  34824  circlemethhgt  34825  hgt750lemg  34836  hgt750lemb  34838  hgt750lema  34839  hgt750leme  34840  tgoldbachgtde  34842  tgoldbachgt  34845  kur14lem7  35432  brtpid2  35942  rabren3dioph  43176  oenord1ex  43676  oenord1  43677  fourierdlem102  46570  fourierdlem114  46582  etransclem48  46644  usgrexmpl1tri  48389  usgrexmpl2nb0  48395  usgrexmpl2nb1  48396  usgrexmpl2nb2  48397  usgrexmpl2nb3  48398  usgrexmpl2nb4  48399  usgrexmpl2nb5  48400