Theorem tpid2 4795

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

Syntax hints:   ∨ w3o 1086   = wceq 1537   ∈ wcel 2103  Vcvv 3482  {ctp 4652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3484  df-un 3975  df-sn 4649  df-pr 4651  df-tp 4653

This theorem is referenced by:  hash3tpb  14540  wrdl3s3  15007  wwlks2onv  29977  elwwlks2ons3im  29978  umgrwwlks2on  29981  s3rnOLD  32904  cyc3evpm  33135  sgnsf  33147  sgncl  34495  signsw0glem  34522  signsw0g  34525  signswmnd  34526  signswrid  34527  prodfzo03  34572  circlevma  34611  circlemethhgt  34612  hgt750lemg  34623  hgt750lemb  34625  hgt750lema  34626  hgt750leme  34627  tgoldbachgtde  34629  tgoldbachgt  34632  kur14lem7  35172  brtpid2  35676  rabren3dioph  42708  oenord1ex  43217  oenord1  43218  fourierdlem102  46063  fourierdlem114  46075  etransclem48  46137  usgrexmpl1tri  47759  usgrexmpl2nb0  47765  usgrexmpl2nb1  47766  usgrexmpl2nb2  47767  usgrexmpl2nb3  47768  usgrexmpl2nb4  47769  usgrexmpl2nb5  47770