Theorem tpid2 4795

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

Syntax hints:   ∨ w3o 1086   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {ctp 4652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651  df-tp 4653

This theorem is referenced by:  hash3tpb  14544  wrdl3s3  15011  wwlks2onv  29986  elwwlks2ons3im  29987  umgrwwlks2on  29990  s3rnOLD  32912  cyc3evpm  33143  sgnsf  33155  sgncl  34503  signsw0glem  34530  signsw0g  34533  signswmnd  34534  signswrid  34535  prodfzo03  34580  circlevma  34619  circlemethhgt  34620  hgt750lemg  34631  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgt  34640  kur14lem7  35180  brtpid2  35684  rabren3dioph  42771  oenord1ex  43277  oenord1  43278  fourierdlem102  46129  fourierdlem114  46141  etransclem48  46203  usgrexmpl1tri  47840  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851