| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > tpid3 | 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.) (Proof shortened by JJ, 30-Apr-2021.) |
| Ref | Expression |
|---|---|
| tpid3.1 | ⊢ 𝐶 ∈ V |
| Ref | Expression |
|---|---|
| tpid3 | ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tpid3.1 | . 2 ⊢ 𝐶 ∈ V | |
| 2 | tpid3g 4772 | . 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶} |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ 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: hash3tpb 14534 wrdl3s3 15001 umgrwwlks2on 29977 ex-pss 30447 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 brtpid3 35723 rabren3dioph 42826 oenord1ex 43328 fourierdlem114 46235 usgrexmpl1tri 47984 usgrexmpl2nb0 47990 usgrexmpl2nb1 47991 usgrexmpl2nb2 47992 usgrexmpl2nb3 47993 usgrexmpl2nb4 47994 usgrexmpl2nb5 47995 gpg3kgrtriex 48045 |
| Copyright terms: Public domain | W3C validator |