Theorem tpid2 4730

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3444  {ctp 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-pr 4588  df-tp 4590

This theorem is referenced by:  hash3tpb  14436  wrdl3s3  14904  wwlks2onv  29933  elwwlks2ons3im  29934  umgrwwlks2on  29937  sgncl  32806  s3rnOLD  32917  cyc3evpm  33122  sgnsf  33134  signsw0glem  34537  signsw0g  34540  signswmnd  34541  signswrid  34542  prodfzo03  34587  circlevma  34626  circlemethhgt  34627  hgt750lemg  34638  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  tgoldbachgtde  34644  tgoldbachgt  34647  kur14lem7  35192  brtpid2  35702  rabren3dioph  42796  oenord1ex  43297  oenord1  43298  fourierdlem102  46199  fourierdlem114  46211  etransclem48  46273  usgrexmpl1tri  48009  usgrexmpl2nb0  48015  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020