Theorem tpid2 4742

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3455  {ctp 4601

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3457  df-un 3927  df-sn 4598  df-pr 4600  df-tp 4602

This theorem is referenced by:  hash3tpb  14470  wrdl3s3  14938  wwlks2onv  29890  elwwlks2ons3im  29891  umgrwwlks2on  29894  sgncl  32764  s3rnOLD  32875  cyc3evpm  33115  sgnsf  33127  signsw0glem  34552  signsw0g  34555  signswmnd  34556  signswrid  34557  prodfzo03  34602  circlevma  34641  circlemethhgt  34642  hgt750lemg  34653  hgt750lemb  34655  hgt750lema  34656  hgt750leme  34657  tgoldbachgtde  34659  tgoldbachgt  34662  kur14lem7  35201  brtpid2  35706  rabren3dioph  42775  oenord1ex  43276  oenord1  43277  fourierdlem102  46179  fourierdlem114  46191  etransclem48  46253  usgrexmpl1tri  47971  usgrexmpl2nb0  47977  usgrexmpl2nb1  47978  usgrexmpl2nb2  47979  usgrexmpl2nb3  47980  usgrexmpl2nb4  47981  usgrexmpl2nb5  47982