Theorem tpid2 4736

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {ctp 4595

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-sn 4592  df-pr 4594  df-tp 4596

This theorem is referenced by:  hash3tpb  14466  wrdl3s3  14934  wwlks2onv  29889  elwwlks2ons3im  29890  umgrwwlks2on  29893  sgncl  32762  s3rnOLD  32873  cyc3evpm  33113  sgnsf  33125  signsw0glem  34550  signsw0g  34553  signswmnd  34554  signswrid  34555  prodfzo03  34600  circlevma  34639  circlemethhgt  34640  hgt750lemg  34651  hgt750lemb  34653  hgt750lema  34654  hgt750leme  34655  tgoldbachgtde  34657  tgoldbachgt  34660  kur14lem7  35199  brtpid2  35704  rabren3dioph  42796  oenord1ex  43297  oenord1  43298  fourierdlem102  46199  fourierdlem114  46211  etransclem48  46273  usgrexmpl1tri  48006  usgrexmpl2nb0  48012  usgrexmpl2nb1  48013  usgrexmpl2nb2  48014  usgrexmpl2nb3  48015  usgrexmpl2nb4  48016  usgrexmpl2nb5  48017