Theorem unisn2

Description: A version of unisn without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006)

	Ref	Expression
Assertion	unisn2	|- U. { A } e. { (/) , A }

Proof

Step	Hyp	Ref	Expression
1		unisng	|- ( A e. _V -> U. { A } = A )
2		prid2g	|- ( A e. _V -> A e. { (/) , A } )
3	1 2	eqeltrd	|- ( A e. _V -> U. { A } e. { (/) , A } )
4		snprc	|- ( -. A e. _V <-> { A } = (/) )
5	4	biimpi	|- ( -. A e. _V -> { A } = (/) )
6	5	unieqd	|- ( -. A e. _V -> U. { A } = U. (/) )
7		uni0	|- U. (/) = (/)
8		0ex	|- (/) e. _V
9	8	prid1	|- (/) e. { (/) , A }
10	7 9	eqeltri	|- U. (/) e. { (/) , A }
11	6 10	eqeltrdi	|- ( -. A e. _V -> U. { A } e. { (/) , A } )
12	3 11	pm2.61i	|- U. { A } e. { (/) , A }