Metamath Proof Explorer

Theorem undefne0

Description: The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018)

Ref Expression
Assertion undefne0 
|- ( S e. V -> ( Undef ` S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 undefval 
 |-  ( S e. V -> ( Undef ` S ) = ~P U. S )
2 pwne0 
 |-  ~P U. S =/= (/)
3 2 a1i 
 |-  ( S e. V -> ~P U. S =/= (/) )
4 1 3 eqnetrd 
 |-  ( S e. V -> ( Undef ` S ) =/= (/) )