Theorem tpid2 4722

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3436  {ctp 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580  df-tp 4582

This theorem is referenced by:  hash3tpb  14402  wrdl3s3  14869  wwlks2onv  29898  elwwlks2ons3im  29899  umgrwwlks2on  29902  sgncl  32777  s3rnOLD  32888  cyc3evpm  33093  sgnsf  33105  signsw0glem  34527  signsw0g  34530  signswmnd  34531  signswrid  34532  prodfzo03  34577  circlevma  34616  circlemethhgt  34617  hgt750lemg  34628  hgt750lemb  34630  hgt750lema  34631  hgt750leme  34632  tgoldbachgtde  34634  tgoldbachgt  34637  kur14lem7  35195  brtpid2  35705  rabren3dioph  42798  oenord1ex  43298  oenord1  43299  fourierdlem102  46199  fourierdlem114  46211  etransclem48  46273  usgrexmpl1tri  48019  usgrexmpl2nb0  48025  usgrexmpl2nb1  48026  usgrexmpl2nb2  48027  usgrexmpl2nb3  48028  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030