Theorem tpid2 4715

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

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {ctp 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571  df-tp 4573

This theorem is referenced by:  hash3tpb  14419  wrdl3s3  14886  wwlks2onv  30010  elwwlks2ons3im  30011  usgrwwlks2on  30015  umgrwwlks2on  30016  sgncl  32895  s3rnOLD  33011  cyc3evpm  33216  sgnsf  33228  signsw0glem  34703  signsw0g  34706  signswmnd  34707  signswrid  34708  prodfzo03  34753  circlevma  34792  circlemethhgt  34793  hgt750lemg  34804  hgt750lemb  34806  hgt750lema  34807  hgt750leme  34808  tgoldbachgtde  34810  tgoldbachgt  34813  kur14lem7  35400  brtpid2  35910  rabren3dioph  43246  oenord1ex  43746  oenord1  43747  fourierdlem102  46640  fourierdlem114  46652  etransclem48  46714  usgrexmpl1tri  48459  usgrexmpl2nb0  48465  usgrexmpl2nb1  48466  usgrexmpl2nb2  48467  usgrexmpl2nb3  48468  usgrexmpl2nb4  48469  usgrexmpl2nb5  48470