![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpid1 | 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 |
---|---|
tpid1.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
tpid1 | ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2771 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | 3mix1i 1417 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶) |
3 | tpid1.1 | . . 3 ⊢ 𝐴 ∈ V | |
4 | 3 | eltp 4367 | . 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
5 | 2, 4 | mpbir 221 | 1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∨ w3o 1070 = wceq 1631 ∈ wcel 2145 Vcvv 3351 {ctp 4320 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-un 3728 df-sn 4317 df-pr 4319 df-tp 4321 |
This theorem is referenced by: tpnz 4447 wrdl3s3 13915 cffldtocusgr 26578 umgrwwlks2on 27105 sgnsf 30069 sgncl 30940 prodfzo03 31021 circlevma 31060 circlemethhgt 31061 hgt750lemg 31072 hgt750lemb 31074 hgt750lema 31075 hgt750leme 31076 tgoldbachgtde 31078 tgoldbachgt 31081 kur14lem7 31532 kur14lem9 31534 brtpid1 31940 rabren3dioph 37905 fourierdlem102 40942 fourierdlem114 40954 etransclem48 41016 |
Copyright terms: Public domain | W3C validator |