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

Metamath Proof Explorer

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 }