Step |
Hyp |
Ref |
Expression |
1 |
|
eqcom |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) = 𝑦 ) |
2 |
|
fnbrfvb |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑦 ↔ 𝐵 𝐹 𝑦 ) ) |
3 |
1 2
|
bitrid |
⊢ ( ( 𝐹 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 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = ( 𝐹 “ { 𝐵 } ) ) |