Theorem tpid2 4715

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 4634	. 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))
5	2, 4	mpbir 231	1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {ctp 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571  df-tp 4573

This theorem is referenced by:  hash3tpb  14451  wrdl3s3  14918  wwlks2onv  30039  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  sgncl  32922  s3rnOLD  33024  cyc3evpm  33229  sgnsf  33241  signsw0glem  34716  signsw0g  34719  signswmnd  34720  signswrid  34721  prodfzo03  34766  circlevma  34805  circlemethhgt  34806  hgt750lemg  34817  hgt750lemb  34819  hgt750lema  34820  hgt750leme  34821  tgoldbachgtde  34823  tgoldbachgt  34826  kur14lem7  35413  brtpid2  35923  rabren3dioph  43264  oenord1ex  43764  oenord1  43765  fourierdlem102  46657  fourierdlem114  46669  etransclem48  46731  usgrexmpl1tri  48516  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527