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 1569   ∈ wcel 2144  Vcvv 3450  {ctp 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  1eltp012  12413  hash3tpb  14640  sgncl  15250  degenmgm2nfun  19139  sgnsf  33723  signsw0glem  35182  signsw0g  35185  signswmnd  35186  signswrid  35187  kur14lem7  35977  brtpid2  36487  rabren3dioph  43822  oenord1ex  44317  oenord1  44318  fourierdlem102  47218  fourierdlem114  47230  etransclem48  47292  usgrexmpl1tri  49123  usgrexmpl2nb3  49132  usgrexmpl2nb4  49133  usgrexmpl2nb5  49134