![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpex | Structured version Visualization version GIF version |
Description: An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
Ref | Expression |
---|---|
tpex | ⊢ {𝐴, 𝐵, 𝐶} ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-tp 4215 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | prex 4939 | . . 3 ⊢ {𝐴, 𝐵} ∈ V | |
3 | snex 4938 | . . 3 ⊢ {𝐶} ∈ V | |
4 | 2, 3 | unex 6998 | . 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V |
5 | 1, 4 | eqeltri 2726 | 1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 Vcvv 3231 ∪ cun 3605 {csn 4210 {cpr 4212 {ctp 4214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 ax-un 6991 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-v 3233 df-dif 3610 df-un 3612 df-nul 3949 df-sn 4211 df-pr 4213 df-tp 4215 df-uni 4469 |
This theorem is referenced by: fr3nr 7021 en3lp 8551 prdsval 16162 imasval 16218 fnfuc 16652 fucval 16665 setcval 16774 catcval 16793 estrcval 16811 estrreslem1 16824 estrres 16826 fnxpc 16863 xpcval 16864 symgval 17845 psrval 19410 xrsex 19809 om1val 22876 signswbase 30759 signswplusg 30760 ldualset 34730 erngset 36405 erngset-rN 36413 dvaset 36610 dvhset 36687 hlhilset 37543 rabren3dioph 37696 mendval 38070 clsk1indlem4 38659 clsk1indlem1 38660 rngcvalALTV 42286 ringcvalALTV 42332 lmod1zrnlvec 42608 |
Copyright terms: Public domain | W3C validator |