tpid3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tpid3		Structured version Visualization version GIF version

Theorem tpid3 4782

Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.)

**Hypothesis**
Ref	Expression
tpid3.1	⊢ 𝐶 ∈ V

**Assertion**
Ref	Expression
tpid3	⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

**Proof of Theorem tpid3**
Step	Hyp	Ref	Expression
1		tpid3.1	. 2 ⊢ 𝐶 ∈ V
2		tpid3g 4781	. 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶})
3	1, 2	ax-mp 5	1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2098 Vcvv 3473 {ctp 4636

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3475 df-un 3954 df-sn 4633 df-pr 4635 df-tp 4637

This theorem is referenced by: wrdl3s3 14953 umgrwwlks2on 29788 ex-pss 30258 s3rn 32690 cyc3evpm 32892 sgnsf 32904 sgncl 34191 prodfzo03 34268 circlevma 34307 circlemethhgt 34308 hgt750lemg 34319 hgt750lemb 34321 hgt750lema 34322 hgt750leme 34323 tgoldbachgtde 34325 tgoldbachgt 34328 kur14lem7 34855 brtpid3 35350 rabren3dioph 42266 oenord1ex 42775 fourierdlem114 45637

W3C validator

	
		OSZAR »