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 2824 | . . 3 ⊢ 𝐵 = 𝐵 | |
2 | 1 | 3mix2i 1330 | . 2 ⊢ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶) |
3 | tpid2.1 | . . 3 ⊢ 𝐵 ∈ V | |
4 | 3 | eltp 4629 | . 2 ⊢ (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)) |
5 | 2, 4 | mpbir 233 | 1 ⊢ 𝐵 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1082 = wceq 1536 ∈ wcel 2113 Vcvv 3497 {ctp 4574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-un 3944 df-sn 4571 df-pr 4573 df-tp 4575 |
This theorem is referenced by: wrdl3s3 14329 wwlks2onv 27735 elwwlks2ons3im 27736 umgrwwlks2on 27739 s3rn 30626 cyc3evpm 30796 sgnsf 30808 sgncl 31800 signsw0glem 31827 signsw0g 31830 signswmnd 31831 signswrid 31832 prodfzo03 31878 circlevma 31917 circlemethhgt 31918 hgt750lemg 31929 hgt750lemb 31931 hgt750lema 31932 hgt750leme 31933 tgoldbachgtde 31935 tgoldbachgt 31938 kur14lem7 32463 brtpid2 32956 rabren3dioph 39418 fourierdlem102 42500 fourierdlem114 42512 etransclem48 42574 |
Copyright terms: Public domain | W3C validator |