Metamath Proof Explorer

Theorem elfv2ex

Description: If a function value of a function value has a member, then the first argument is a set. (Contributed by AV, 8-Apr-2021)

Ref Expression
Assertion elfv2ex 
|- ( A e. ( ( F ` B ) ` C ) -> B e. _V )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( B e. _V -> ( A e. ( ( F ` B ) ` C ) -> B e. _V ) )
2 fv2prc 
 |-  ( -. B e. _V -> ( ( F ` B ) ` C ) = (/) )
3 2 eleq2d 
 |-  ( -. B e. _V -> ( A e. ( ( F ` B ) ` C ) <-> A e. (/) ) )
4 noel 
 |-  -. A e. (/)
5 4 pm2.21i 
 |-  ( A e. (/) -> B e. _V )
6 3 5 biimtrdi 
 |-  ( -. B e. _V -> ( A e. ( ( F ` B ) ` C ) -> B e. _V ) )
7 1 6 pm2.61i 
 |-  ( A e. ( ( F ` B ) ` C ) -> B e. _V )