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 }