Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > tpid3 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
tpid3.1 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
tpid3 | ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpid3.1 | . 2 ⊢ 𝐶 ∈ V | |
2 | tpid3g 4720 | . 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3441 {ctp 4577 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3443 df-un 3903 df-sn 4574 df-pr 4576 df-tp 4578 |
This theorem is referenced by: wrdl3s3 14776 umgrwwlks2on 28610 ex-pss 29080 s3rn 31507 cyc3evpm 31704 sgnsf 31716 sgncl 32805 prodfzo03 32883 circlevma 32922 circlemethhgt 32923 hgt750lemg 32934 hgt750lemb 32936 hgt750lema 32937 hgt750leme 32938 tgoldbachgtde 32940 tgoldbachgt 32943 kur14lem7 33473 brtpid3 33964 rabren3dioph 40899 fourierdlem114 44097 |
Copyright terms: Public domain | W3C validator |