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 ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → { ( 𝐹𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 eqcom ( 𝑦 = ( 𝐹𝐵 ) ↔ ( 𝐹𝐵 ) = 𝑦 )
2 fnbrfvb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = 𝑦𝐵 𝐹 𝑦 ) )
3 1 2 syl5bb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝑦 = ( 𝐹𝐵 ) ↔ 𝐵 𝐹 𝑦 ) )
4 3 abbidv ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → { 𝑦𝑦 = ( 𝐹𝐵 ) } = { 𝑦𝐵 𝐹 𝑦 } )
5 df-sn { ( 𝐹𝐵 ) } = { 𝑦𝑦 = ( 𝐹𝐵 ) }
6 5 a1i ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → { ( 𝐹𝐵 ) } = { 𝑦𝑦 = ( 𝐹𝐵 ) } )
7 fnrel ( 𝐹 Fn 𝐴 → Rel 𝐹 )
8 relimasn ( Rel 𝐹 → ( 𝐹 “ { 𝐵 } ) = { 𝑦𝐵 𝐹 𝑦 } )
9 7 8 syl ( 𝐹 Fn 𝐴 → ( 𝐹 “ { 𝐵 } ) = { 𝑦𝐵 𝐹 𝑦 } )
10 9 adantr ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹 “ { 𝐵 } ) = { 𝑦𝐵 𝐹 𝑦 } )
11 4 6 10 3eqtr4d ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → { ( 𝐹𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )