Theorem tpid2 4711

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

Syntax hints:   ∨ w3o 1084   = wceq 1541   ∈ wcel 2109  Vcvv 3430  {ctp 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-sn 4567  df-pr 4569  df-tp 4571

This theorem is referenced by:  wrdl3s3  14658  wwlks2onv  28297  elwwlks2ons3im  28298  umgrwwlks2on  28301  s3rn  31199  cyc3evpm  31396  sgnsf  31408  sgncl  32484  signsw0glem  32511  signsw0g  32514  signswmnd  32515  signswrid  32516  prodfzo03  32562  circlevma  32601  circlemethhgt  32602  hgt750lemg  32613  hgt750lemb  32615  hgt750lema  32616  hgt750leme  32617  tgoldbachgtde  32619  tgoldbachgt  32622  kur14lem7  33153  brtpid2  33645  rabren3dioph  40617  fourierdlem102  43703  fourierdlem114  43715  etransclem48  43777