Theorem tpid2 4705

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

Syntax hints:   ∨ w3o 1092   = wceq 1548   ∈ wcel 2121  Vcvv 3433  {ctp 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-un 3890  df-sn 4559  df-pr 4561  df-tp 4563

This theorem is referenced by:  hash3tpb  14452  wrdl3s3  14919  wwlks2onv  30043  elwwlks2ons3im  30044  usgrwwlks2on  30048  umgrwwlks2on  30049  sgncl  32927  s3rnOLD  33029  cyc3evpm  33235  sgnsf  33247  signsw0glem  34749  signsw0g  34752  signswmnd  34753  signswrid  34754  prodfzo03  34799  circlevma  34838  circlemethhgt  34839  hgt750lemg  34850  hgt750lemb  34852  hgt750lema  34853  hgt750leme  34854  tgoldbachgtde  34856  tgoldbachgt  34859  kur14lem7  35455  brtpid2  35965  rabren3dioph  43275  oenord1ex  43775  oenord1  43776  fourierdlem102  46665  fourierdlem114  46677  etransclem48  46739  usgrexmpl1tri  48530  usgrexmpl2nb0  48536  usgrexmpl2nb1  48537  usgrexmpl2nb2  48538  usgrexmpl2nb3  48539  usgrexmpl2nb4  48540  usgrexmpl2nb5  48541