![]() |
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 2779 | . . 3 ⊢ 𝐵 = 𝐵 | |
2 | 1 | 3mix2i 1314 | . 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶) |
3 | tpid2.1 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 3 | eltp 4500 | . 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)) |
5 | 2, 4 | mpbir 223 | 1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1067 = wceq 1507 ∈ wcel 2050 Vcvv 3416 {ctp 4445 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-v 3418 df-un 3835 df-sn 4442 df-pr 4444 df-tp 4446 |
This theorem is referenced by: wrdl3s3 14187 wwlks2onv 27459 elwwlks2ons3im 27460 umgrwwlks2on 27463 s3rn 30364 sgnsf 30467 sgncl 31439 signsw0glem 31466 signsw0g 31469 signswmnd 31470 signswrid 31471 prodfzo03 31519 circlevma 31558 circlemethhgt 31559 hgt750lemg 31570 hgt750lemb 31572 hgt750lema 31573 hgt750leme 31574 tgoldbachgtde 31576 tgoldbachgt 31579 kur14lem7 32041 brtpid2 32469 rabren3dioph 38805 fourierdlem102 41922 fourierdlem114 41934 etransclem48 41996 |
Copyright terms: Public domain | W3C validator |