vsnex - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vsnex		Structured version Visualization version GIF version

Theorem vsnex 5426

Description: A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)

**Assertion**
Ref	Expression
vsnex	⊢ {𝑥} ∈ V

**Proof of Theorem vsnex**
Step	Hyp	Ref	Expression
1		dfsn2 4638	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5425	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2825	1 ⊢ {𝑥} ∈ V

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2099 Vcvv 3470 {csn 4625 {cpr 4627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5294 ax-pr 5424

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3472 df-un 3950 df-sn 4626 df-pr 4628

This theorem is referenced by: snexg 5427 rext 5445 sspwb 5446 moabex 5456 nnullss 5459 exss 5460 xpsspw 5806 funopg 6582 snnex 7755 soex 7924 opabex3d 7964 opabex3rd 7965 opabex3 7966 fo1st 8008 fo2nd 8009 mpoexxg 8075 cnvf1o 8111 sexp2 8146 sexp3 8153 naddcllem 8691 domunsn 9146 fodomr 9147 findcard2 9183 pwfilem 9196 marypha1lem 9451 brwdom2 9591 unxpwdom2 9606 elirrv 9614 epfrs 9749 dfac5lem2 10142 dfac5lem3 10143 dfac5lem4 10144 kmlem2 10169 isfin1-3 10404 hsmexlem4 10447 axcc2lem 10454 canthwe 10669 canthp1lem1 10670 uniwun 10758 rankcf 10795 hashmap 14421 hashbclem 14438 incexclem 15809 isfunc 17844 homaf 18013 symgvalstruct 19345 gsum2d2 19923 gsumcom2 19924 dprd2da 19993 mpfind 22047 pf1ind 22268 dishaus 23280 discmp 23296 dis2ndc 23358 dislly 23395 dis1stc 23397 unisngl 23425 1stckgen 23452 ptcmpfi 23711 isufil2 23806 cnextfval 23960 conway 27726 etasslt 27740 cofcutr 27838 lfuhgr1v0e 29061 gsumpart 32764 esum2dlem 33706 esum2d 33707 esumiun 33708 carsgclctunlem1 33932 eulerpartlemgs2 33995 bnj1452 34678 fobigcup 35491 elsingles 35509 fnsingle 35510 fvsingle 35511 dfiota3 35514 funpartlem 35533 altxpsspw 35568 bj-snsetex 36437 bj-elsngl 36442 f1omptsnlem 36810 mptsnunlem 36812 topdifinffinlem 36821 heiborlem3 37281 ispointN 39210 mzpincl 42145 mzpcompact2lem 42162 pwslnmlem1 42507 pwslnm 42509 mpct 44565 salexct3 45721 salgencntex 45722 salgensscntex 45723 sge0xp 45808 mpoexxg2 47392

	
		OSZAR »