Theorem tpid2 4731

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

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {ctp 4592

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591  df-tp 4593

This theorem is used by:  1eltp012  12437  hash3tpb  14664  sgncl  15276  degenmgm2nfun  19165  sgnsf  33790  signsw0glem  35249  signsw0g  35252  signswmnd  35253  signswrid  35254  kur14lem7  36143  brtpid2  36664  rabren3dioph  44013  oenord1ex  44507  oenord1  44508  fourierdlem102  47421  fourierdlem114  47433  etransclem48  47495  usgrexmpl1tri  49326  usgrexmpl2nb3  49335  usgrexmpl2nb4  49336  usgrexmpl2nb5  49337