Metamath Proof Explorer

Theorem afvvv

Description: If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afvvv 
|- ( ( F ''' A ) e. B -> A e. _V )

Proof

Step Hyp Ref Expression
1 afvprc 
 |-  ( -. A e. _V -> ( F ''' A ) = _V )
2 nvelim 
 |-  ( ( F ''' A ) = _V -> -. ( F ''' A ) e. B )
3 1 2 syl 
 |-  ( -. A e. _V -> -. ( F ''' A ) e. B )
4 3 con4i 
 |-  ( ( F ''' A ) e. B -> A e. _V )