This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , (/) )