Theorem bj-snglss

Description: The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglss	|- sngl A C_ ~P A

Proof

Step	Hyp	Ref	Expression
1		bj-elsngl	|- ( x e. sngl A <-> E. y e. A x = { y } )
2		df-rex	|- ( E. y e. A x = { y } <-> E. y ( y e. A /\ x = { y } ) )
3		snssi	|- ( y e. A -> { y } C_ A )
4		sseq1	|- ( x = { y } -> ( x C_ A <-> { y } C_ A ) )
5	4	biimparc	|- ( ( { y } C_ A /\ x = { y } ) -> x C_ A )
6	3 5	sylan	|- ( ( y e. A /\ x = { y } ) -> x C_ A )
7	6	eximi	|- ( E. y ( y e. A /\ x = { y } ) -> E. y x C_ A )
8	2 7	sylbi	|- ( E. y e. A x = { y } -> E. y x C_ A )
9	1 8	sylbi	|- ( x e. sngl A -> E. y x C_ A )
10		ax5e	|- ( E. y x C_ A -> x C_ A )
11	9 10	syl	|- ( x e. sngl A -> x C_ A )
12		velpw	|- ( x e. ~P A <-> x C_ A )
13	11 12	sylibr	|- ( x e. sngl A -> x e. ~P A )
14	13	ssriv	|- sngl A C_ ~P A