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

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  Vcvv 3450  {ctp 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3903  df-sn 4584  df-pr 4586  df-tp 4588

This theorem is used by:  1eltp012  12382  hash3tpb  14607  sgncl  15217  degenmgm2nfun  19100  sgnsf  33656  signsw0glem  35116  signsw0g  35119  signswmnd  35120  signswrid  35121  kur14lem7  35898  brtpid2  36408  rabren3dioph  43760  oenord1ex  44260  oenord1  44261  fourierdlem102  47140  fourierdlem114  47152  etransclem48  47214  usgrexmpl1tri  49045  usgrexmpl2nb3  49054  usgrexmpl2nb4  49055  usgrexmpl2nb5  49056