Theorem tpid2 4770

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

Syntax hints:   ∨ w3o 1084   = wceq 1534   ∈ wcel 2099  Vcvv 3469  {ctp 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949  df-sn 4625  df-pr 4627  df-tp 4629

This theorem is referenced by:  wrdl3s3  14937  wwlks2onv  29751  elwwlks2ons3im  29752  umgrwwlks2on  29755  s3rn  32651  cyc3evpm  32849  sgnsf  32861  sgncl  34094  signsw0glem  34121  signsw0g  34124  signswmnd  34125  signswrid  34126  prodfzo03  34171  circlevma  34210  circlemethhgt  34211  hgt750lemg  34222  hgt750lemb  34224  hgt750lema  34225  hgt750leme  34226  tgoldbachgtde  34228  tgoldbachgt  34231  kur14lem7  34758  brtpid2  35252  rabren3dioph  42157  oenord1ex  42667  oenord1  42668  fourierdlem102  45519  fourierdlem114  45531  etransclem48  45593