Theorem tpid1 4488

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 2802	. . 3 ⊢ 𝐴 = 𝐴
2	1	3mix1i 1425	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)
3		tpid1.1	. . 3 ⊢ 𝐴 ∈ V
4	3	eltp 4416	. 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	2, 4	mpbir 222	1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∨ w3o 1099   = wceq 1637   ∈ wcel 2155  Vcvv 3387  {ctp 4368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-un 3768  df-sn 4365  df-pr 4367  df-tp 4369

This theorem is referenced by:  tpnz  4496  wrdl3s3  13924  cffldtocusgr  26565  umgrwwlks2on  27092  sgnsf  30048  sgncl  30919  prodfzo03  31000  circlevma  31039  circlemethhgt  31040  hgt750lemg  31051  hgt750lemb  31053  hgt750lema  31054  hgt750leme  31055  tgoldbachgtde  31057  tgoldbachgt  31060  kur14lem7  31511  kur14lem9  31513  brtpid1  31918  rabren3dioph  37875  fourierdlem102  40898  fourierdlem114  40910  etransclem48  40972