Theorem tpid2 4720

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

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {ctp 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576  df-tp 4578

This theorem is referenced by:  hash3tpb  14402  wrdl3s3  14869  wwlks2onv  29931  elwwlks2ons3im  29932  usgrwwlks2on  29936  umgrwwlks2on  29937  sgncl  32814  s3rnOLD  32927  cyc3evpm  33119  sgnsf  33131  signsw0glem  34566  signsw0g  34569  signswmnd  34570  signswrid  34571  prodfzo03  34616  circlevma  34655  circlemethhgt  34656  hgt750lemg  34667  hgt750lemb  34669  hgt750lema  34670  hgt750leme  34671  tgoldbachgtde  34673  tgoldbachgt  34676  kur14lem7  35256  brtpid2  35766  rabren3dioph  42918  oenord1ex  43418  oenord1  43419  fourierdlem102  46316  fourierdlem114  46328  etransclem48  46390  usgrexmpl1tri  48135  usgrexmpl2nb0  48141  usgrexmpl2nb1  48142  usgrexmpl2nb2  48143  usgrexmpl2nb3  48144  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146