Metamath Proof Explorer


Theorem fnsnfvOLD

Description: Obsolete version of fnsnfv as of 8-Aug-2024. (Contributed by NM, 22-May-1998) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion fnsnfvOLD
|- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )

Proof

Step Hyp Ref Expression
1 eqcom
 |-  ( y = ( F ` B ) <-> ( F ` B ) = y )
2 fnbrfvb
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = y <-> B F y ) )
3 1 2 syl5bb
 |-  ( ( F Fn A /\ B e. A ) -> ( y = ( F ` B ) <-> B F y ) )
4 3 abbidv
 |-  ( ( F Fn A /\ B e. A ) -> { y | y = ( F ` B ) } = { y | B F y } )
5 df-sn
 |-  { ( F ` B ) } = { y | y = ( F ` B ) }
6 5 a1i
 |-  ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = { y | y = ( F ` B ) } )
7 fnrel
 |-  ( F Fn A -> Rel F )
8 relimasn
 |-  ( Rel F -> ( F " { B } ) = { y | B F y } )
9 7 8 syl
 |-  ( F Fn A -> ( F " { B } ) = { y | B F y } )
10 9 adantr
 |-  ( ( F Fn A /\ B e. A ) -> ( F " { B } ) = { y | B F y } )
11 4 6 10 3eqtr4d
 |-  ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )