| 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 2737 | . . 3 ⊢ 𝐴 = 𝐴 | |
| 2 | 1 | 3mix1i 1334 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶) |
| 3 | tpid1.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 4 | 3 | eltp 4689 | . 2 ⊢ (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
| 5 | 2, 4 | mpbir 231 | 1 ⊢ 𝐴 ∈ {𝐴, 𝐵, 𝐶} |
| Colors of variables: wff setvar class |
| Syntax hints: ∨ w3o 1086 = wceq 1540 ∈ wcel 2108 Vcvv 3480 {ctp 4630 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 df-tp 4631 |
| This theorem is referenced by: tpnz 4779 hash3tpb 14534 wrdl3s3 15001 cffldtocusgr 29464 cffldtocusgrOLD 29465 umgrwwlks2on 29977 s3rnOLD 32930 cyc3evpm 33170 sgnsf 33182 sgncl 34541 prodfzo03 34618 circlevma 34657 circlemethhgt 34658 hgt750lemg 34669 hgt750lemb 34671 hgt750lema 34672 hgt750leme 34673 tgoldbachgtde 34675 tgoldbachgt 34678 kur14lem7 35217 kur14lem9 35219 brtpid1 35721 rabren3dioph 42826 fourierdlem102 46223 fourierdlem114 46235 etransclem48 46297 usgrexmpl1tri 47984 usgrexmpl2nb0 47990 usgrexmpl2nb1 47991 usgrexmpl2nb2 47992 usgrexmpl2nb3 47993 usgrexmpl2nb4 47994 usgrexmpl2nb5 47995 gpg3kgrtriex 48045 |
| Copyright terms: Public domain | W3C validator |