Theorem unisnif

Description: Express union of singleton in terms of if . (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	unisnif	|- U. { A } = if ( A e. _V , A , (/) )

Proof

Step	Hyp	Ref	Expression
1		iftrue	|- ( A e. _V -> if ( A e. _V , A , (/) ) = A )
2		unisng	|- ( A e. _V -> U. { A } = A )
3	1 2	eqtr4d	|- ( A e. _V -> if ( A e. _V , A , (/) ) = U. { A } )
4		iffalse	|- ( -. A e. _V -> if ( A e. _V , A , (/) ) = (/) )
5		snprc	|- ( -. A e. _V <-> { A } = (/) )
6	5	biimpi	|- ( -. A e. _V -> { A } = (/) )
7	6	unieqd	|- ( -. A e. _V -> U. { A } = U. (/) )
8		uni0	|- U. (/) = (/)
9	7 8	eqtrdi	|- ( -. A e. _V -> U. { A } = (/) )
10	4 9	eqtr4d	|- ( -. A e. _V -> if ( A e. _V , A , (/) ) = U. { A } )
11	3 10	pm2.61i	|- if ( A e. _V , A , (/) ) = U. { A }
12	11	eqcomi	|- U. { A } = if ( A e. _V , A , (/) )