Theorem tpid1 4730

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

Syntax hints:   ∨ w3o 1100   = wceq 1563   ∈ wcel 2145  Vcvv 3457  {ctp 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588  df-tp 4590

This theorem is referenced by:  tpnz  4741  hash3tpb  14522  wrdl3s3  14989  sgncl  15124  cffldtocusgr  29706  usgrwwlks2on  30216  umgrwwlks2on  30217  s3rnOLD  33179  cyc3evpm  33383  sgnsf  33395  prodfzo03  34907  circlevma  34946  circlemethhgt  34947  hgt750lemg  34958  hgt750lemb  34960  hgt750lema  34961  hgt750leme  34962  tgoldbachgtde  34964  tgoldbachgt  34967  kur14lem7  35575  kur14lem9  35577  brtpid1  36084  rabren3dioph  43404  fourierdlem102  46780  fourierdlem114  46792  etransclem48  46854  usgrexmpl1tri  48645  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  gpg3kgrtriex  48709