| 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 4631 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
| 2 | prex 5437 | . . 3 ⊢ {𝐴, 𝐵} ∈ V | |
| 3 | snex 5436 | . . 3 ⊢ {𝐶} ∈ V | |
| 4 | 2, 3 | unex 7764 | . 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V |
| 5 | 1, 4 | eqeltri 2837 | 1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ∪ cun 3949 {csn 4626 {cpr 4628 {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 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-sn 4627 df-pr 4629 df-tp 4631 df-uni 4908 |
| This theorem is referenced by: fr3nr 7792 en3lp 9654 prdsval 17500 imasval 17556 fnfuc 17993 fucval 18006 setcval 18122 catcval 18145 estrcval 18168 estrreslem1 18181 estrreslem1OLD 18182 estrres 18184 fnxpc 18221 xpcval 18222 efmnd 18883 cnfldex 21367 xrsex 21395 psrval 21935 om1val 25063 rlocbas 33271 rlocaddval 33272 rlocmulval 33273 idlsrgval 33531 evl1deg2 33602 signswbase 34569 signswplusg 34570 ldualset 39126 erngset 40802 erngset-rN 40810 dvaset 41007 dvhset 41083 hlhilset 41936 rabren3dioph 42826 mendval 43191 clsk1indlem4 44057 clsk1indlem1 44058 grtrimap 47915 usgrgrtrirex 47917 grlimgrtri 47963 rngcvalALTV 48181 ringcvalALTV 48205 lmod1zrnlvec 48411 mndtcval 49176 |
| Copyright terms: Public domain | W3C validator |