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 2761	. . 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 2145  Vcvv 3451  {ctp 4588

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is used by:  tpnz  4740  hash3tpb  14620  s3rex  15081  wrdl3s3  15095  sgncl  15230  elcgrabasi  29357  cffldtocusgr  30010  usgrwwlks2on  30529  umgrwwlks2on  30530  cyc3evpm  33693  sgnsf  33705  prodfzo03  35215  circlevma  35254  circlemethhgt  35255  hgt750lemg  35266  hgt750lemb  35268  hgt750lema  35269  hgt750leme  35270  tgoldbachgtde  35272  tgoldbachgt  35275  kur14lem7  35946  kur14lem9  35948  brtpid1  36455  rabren3dioph  43775  fourierdlem102  47162  fourierdlem114  47174  etransclem48  47236  usgrexmpl1tri  49067  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  gpg3kgrtriex  49131