Theorem tpid1 4707

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

Syntax hints:   ∨ w3o 1091   = wceq 1547   ∈ wcel 2119  Vcvv 3432  {ctp 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565  df-tp 4567

This theorem is referenced by:  tpnz  4718  hash3tpb  14455  wrdl3s3  14922  cffldtocusgr  29541  usgrwwlks2on  30051  umgrwwlks2on  30052  sgncl  32930  s3rnOLD  33032  cyc3evpm  33238  sgnsf  33250  prodfzo03  34794  circlevma  34833  circlemethhgt  34834  hgt750lemg  34845  hgt750lemb  34847  hgt750lema  34848  hgt750leme  34849  tgoldbachgtde  34851  tgoldbachgt  34854  kur14lem7  35447  kur14lem9  35449  brtpid1  35956  rabren3dioph  43267  fourierdlem102  46658  fourierdlem114  46670  etransclem48  46732  usgrexmpl1tri  48523  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  gpg3kgrtriex  48587