Theorem tpid1 4729

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
tpid1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
tpid1	⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid1

Step	Hyp	Ref	Expression
1		eqid 2763	. . 3 ⊢ 𝐴 = 𝐴
2	1	3mix1i 1352	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)
3		tpid1.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:  tpnz  4740  hash3tpb  14670  s3rex  15133  wrdl3s3  15147  sgncl  15282  elcgrabasi  29408  cffldtocusgr  30061  usgrwwlks2on  30580  umgrwwlks2on  30581  cyc3evpm  33787  sgnsf  33799  prodfzo03  35315  circlevma  35354  circlemethhgt  35355  hgt750lemg  35366  hgt750lemb  35368  hgt750lema  35369  hgt750leme  35370  tgoldbachgtde  35372  tgoldbachgt  35375  kur14lem7  36157  kur14lem9  36159  brtpid1  36677  rabren3dioph  44026  fourierdlem102  47433  fourierdlem114  47445  etransclem48  47507  usgrexmpl1tri  49338  usgrexmpl2nb0  49344  usgrexmpl2nb1  49345  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  gpg3kgrtriex  49402