![]() |
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 4530 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | prex 5298 | . . 3 ⊢ {𝐴, 𝐵} ∈ V | |
3 | snex 5297 | . . 3 ⊢ {𝐶} ∈ V | |
4 | 2, 3 | unex 7449 | . 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V |
5 | 1, 4 | eqeltri 2886 | 1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Vcvv 3441 ∪ cun 3879 {csn 4525 {cpr 4527 {ctp 4529 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-sn 4526 df-pr 4528 df-tp 4530 df-uni 4801 |
This theorem is referenced by: fr3nr 7474 en3lp 9061 prdsval 16720 imasval 16776 fnfuc 17207 fucval 17220 setcval 17329 catcval 17348 estrcval 17366 estrreslem1 17379 estrres 17381 fnxpc 17418 xpcval 17419 efmnd 18027 xrsex 20106 psrval 20600 om1val 23635 idlsrgval 31056 signswbase 31934 signswplusg 31935 ldualset 36421 erngset 38096 erngset-rN 38104 dvaset 38301 dvhset 38377 hlhilset 39230 rabren3dioph 39756 mendval 40127 clsk1indlem4 40747 clsk1indlem1 40748 rngcvalALTV 44585 ringcvalALTV 44631 lmod1zrnlvec 44903 |
Copyright terms: Public domain | W3C validator |