![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpid2 | 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.) |
Ref | Expression |
---|---|
tpid2.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
tpid2 | ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2760 | . . 3 ⊢ 𝐵 = 𝐵 | |
2 | 1 | 3mix2i 1419 | . 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶) |
3 | tpid2.1 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 3 | eltp 4374 | . 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)) |
5 | 2, 4 | mpbir 221 | 1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1071 = wceq 1632 ∈ wcel 2139 Vcvv 3340 {ctp 4325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-un 3720 df-sn 4322 df-pr 4324 df-tp 4326 |
This theorem is referenced by: wrdl3s3 13906 wwlks2onv 27073 elwwlks2ons3im 27074 elwwlks2ons3OLD 27076 umgrwwlks2on 27078 sgnsf 30038 sgncl 30909 signsw0glem 30939 signsw0g 30942 signswmnd 30943 signswrid 30944 prodfzo03 30990 circlevma 31029 circlemethhgt 31030 hgt750lemg 31041 hgt750lemb 31043 hgt750lema 31044 hgt750leme 31045 tgoldbachgtde 31047 tgoldbachgt 31050 kur14lem7 31501 brtpid2 31910 rabren3dioph 37881 fourierdlem102 40928 fourierdlem114 40940 etransclem48 41002 |
Copyright terms: Public domain | W3C validator |