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 4564 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | prex 5324 | . . 3 ⊢ {𝐴, 𝐵} ∈ V | |
3 | snex 5323 | . . 3 ⊢ {𝐶} ∈ V | |
4 | 2, 3 | unex 7457 | . 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V |
5 | 1, 4 | eqeltri 2909 | 1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3495 ∪ cun 3933 {csn 4559 {cpr 4561 {ctp 4563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-v 3497 df-dif 3938 df-un 3940 df-nul 4291 df-sn 4560 df-pr 4562 df-tp 4564 df-uni 4833 |
This theorem is referenced by: fr3nr 7482 en3lp 9066 prdsval 16718 imasval 16774 fnfuc 17205 fucval 17218 setcval 17327 catcval 17346 estrcval 17364 estrreslem1 17377 estrres 17379 fnxpc 17416 xpcval 17417 symgval 18437 psrval 20072 xrsex 20490 om1val 23563 signswbase 31724 signswplusg 31725 ldualset 36143 erngset 37818 erngset-rN 37826 dvaset 38023 dvhset 38099 hlhilset 38952 rabren3dioph 39292 mendval 39663 clsk1indlem4 40274 clsk1indlem1 40275 efmnd 43939 rngcvalALTV 44130 ringcvalALTV 44176 lmod1zrnlvec 44447 |
Copyright terms: Public domain | W3C validator |