Theorem tpid2 4686

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

Syntax hints:   ∨ w3o 1088   = wceq 1543   ∈ wcel 2110  Vcvv 3408  {ctp 4545

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-sn 4542  df-pr 4544  df-tp 4546

This theorem is referenced by:  wrdl3s3  14529  wwlks2onv  28037  elwwlks2ons3im  28038  umgrwwlks2on  28041  s3rn  30940  cyc3evpm  31136  sgnsf  31148  sgncl  32217  signsw0glem  32244  signsw0g  32247  signswmnd  32248  signswrid  32249  prodfzo03  32295  circlevma  32334  circlemethhgt  32335  hgt750lemg  32346  hgt750lemb  32348  hgt750lema  32349  hgt750leme  32350  tgoldbachgtde  32352  tgoldbachgt  32355  kur14lem7  32887  brtpid2  33381  rabren3dioph  40340  fourierdlem102  43424  fourierdlem114  43436  etransclem48  43498