Theorem tpid2 4580

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

Syntax hints:   ∨ w3o 1067   = wceq 1507   ∈ wcel 2050  Vcvv 3416  {ctp 4445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-v 3418  df-un 3835  df-sn 4442  df-pr 4444  df-tp 4446

This theorem is referenced by:  wrdl3s3  14187  wwlks2onv  27459  elwwlks2ons3im  27460  umgrwwlks2on  27463  s3rn  30364  sgnsf  30467  sgncl  31439  signsw0glem  31466  signsw0g  31469  signswmnd  31470  signswrid  31471  prodfzo03  31519  circlevma  31558  circlemethhgt  31559  hgt750lemg  31570  hgt750lemb  31572  hgt750lema  31573  hgt750leme  31574  tgoldbachgtde  31576  tgoldbachgt  31579  kur14lem7  32041  brtpid2  32469  rabren3dioph  38805  fourierdlem102  41922  fourierdlem114  41934  etransclem48  41996