| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vsnex | Structured version Visualization version GIF version | ||
| Description: A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.) |
| Ref | Expression |
|---|---|
| vsnex | ⊢ {𝑥} ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfsn2 4639 | . 2 ⊢ {𝑥} = {𝑥, 𝑥} | |
| 2 | zfpair2 5433 | . 2 ⊢ {𝑥, 𝑥} ∈ V | |
| 3 | 1, 2 | eqeltri 2837 | 1 ⊢ {𝑥} ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 {csn 4626 {cpr 4628 |
| 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-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 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 |
| This theorem is referenced by: snexg 5435 rext 5453 sspwb 5454 moabex 5464 nnullss 5467 exss 5468 xpsspw 5819 funopg 6600 snnex 7778 soex 7943 opabex3d 7990 opabex3rd 7991 opabex3 7992 fo1st 8034 fo2nd 8035 mpoexxg 8100 cnvf1o 8136 sexp2 8171 sexp3 8178 naddcllem 8714 domunsn 9167 fodomr 9168 findcard2 9204 pwfilem 9356 marypha1lem 9473 brwdom2 9613 unxpwdom2 9628 elirrv 9636 epfrs 9771 dfac5lem2 10164 dfac5lem3 10165 dfac5lem4 10166 dfac5lem4OLD 10168 kmlem2 10192 isfin1-3 10426 hsmexlem4 10469 axcc2lem 10476 canthwe 10691 canthp1lem1 10692 uniwun 10780 rankcf 10817 hashmap 14474 hashbclem 14491 incexclem 15872 isfunc 17909 homaf 18075 symgvalstruct 19414 gsum2d2 19992 gsumcom2 19993 dprd2da 20062 mpfind 22131 pf1ind 22359 dishaus 23390 discmp 23406 dis2ndc 23468 dislly 23505 dis1stc 23507 unisngl 23535 1stckgen 23562 ptcmpfi 23821 isufil2 23916 cnextfval 24070 conway 27844 etasslt 27858 cofcutr 27958 lfuhgr1v0e 29271 gsumpart 33060 gsumwrd2dccat 33070 esum2dlem 34093 esum2d 34094 esumiun 34095 carsgclctunlem1 34319 eulerpartlemgs2 34382 bnj1452 35066 fobigcup 35901 elsingles 35919 fnsingle 35920 fvsingle 35921 dfiota3 35924 funpartlem 35943 altxpsspw 35978 bj-snsetex 36964 bj-elsngl 36969 f1omptsnlem 37337 mptsnunlem 37339 topdifinffinlem 37348 heiborlem3 37820 ispointN 39744 mzpincl 42745 mzpcompact2lem 42762 pwslnmlem1 43104 pwslnm 43106 mpct 45206 salexct3 46357 salgencntex 46358 salgensscntex 46359 sge0xp 46444 clnbgrval 47809 mpoexxg2 48254 tposideq 48788 |
| Copyright terms: Public domain | W3C validator |