Metamath Proof Explorer

Theorem pwuninel2

Description: Direct proof of pwuninel avoiding functions and thus several ZF axioms. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion pwuninel2 
|- ( U. A e. V -> -. ~P U. A e. A )

Proof

Step Hyp Ref Expression
1 pwnss 
 |-  ( U. A e. V -> -. ~P U. A C_ U. A )
2 elssuni 
 |-  ( ~P U. A e. A -> ~P U. A C_ U. A )
3 1 2 nsyl 
 |-  ( U. A e. V -> -. ~P U. A e. A )