Theorem tpid2 4775

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

Syntax hints:   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098  Vcvv 3463  {ctp 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-un 3950  df-sn 4630  df-pr 4632  df-tp 4634

This theorem is referenced by:  wrdl3s3  14945  wwlks2onv  29820  elwwlks2ons3im  29821  umgrwwlks2on  29824  s3rn  32726  cyc3evpm  32928  sgnsf  32940  sgncl  34228  signsw0glem  34255  signsw0g  34258  signswmnd  34259  signswrid  34260  prodfzo03  34305  circlevma  34344  circlemethhgt  34345  hgt750lemg  34356  hgt750lemb  34358  hgt750lema  34359  hgt750leme  34360  tgoldbachgtde  34362  tgoldbachgt  34365  kur14lem7  34892  brtpid2  35386  rabren3dioph  42300  oenord1ex  42809  oenord1  42810  fourierdlem102  45659  fourierdlem114  45671  etransclem48  45733