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 2736 | . . 3 ⊢ 𝐵 = 𝐵 | |
2 | 1 | 3mix2i 1333 | . 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶) |
3 | tpid2.1 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 3 | eltp 4635 | . 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)) |
5 | 2, 4 | mpbir 230 | 1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1085 = wceq 1540 ∈ wcel 2105 Vcvv 3441 {ctp 4576 |
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 3902 df-sn 4573 df-pr 4575 df-tp 4577 |
This theorem is referenced by: wrdl3s3 14768 wwlks2onv 28547 elwwlks2ons3im 28548 umgrwwlks2on 28551 s3rn 31448 cyc3evpm 31645 sgnsf 31657 sgncl 32746 signsw0glem 32773 signsw0g 32776 signswmnd 32777 signswrid 32778 prodfzo03 32824 circlevma 32863 circlemethhgt 32864 hgt750lemg 32875 hgt750lemb 32877 hgt750lema 32878 hgt750leme 32879 tgoldbachgtde 32881 tgoldbachgt 32884 kur14lem7 33414 brtpid2 33904 rabren3dioph 40887 fourierdlem102 44074 fourierdlem114 44086 etransclem48 44148 |
Copyright terms: Public domain | W3C validator |