Step |
Hyp |
Ref |
Expression |
1 |
|
feu |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 〈 𝑋 , 𝑦 〉 ∈ 𝐹 ) |
2 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 ) |
3 |
2
|
anim1i |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) |
5 |
|
fnopfvb |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ 〈 𝑋 , 𝑦 〉 ∈ 𝐹 ) ) |
6 |
4 5
|
syl |
⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ 〈 𝑋 , 𝑦 〉 ∈ 𝐹 ) ) |
7 |
6
|
reubidva |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ∃! 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ ∃! 𝑦 ∈ 𝐵 〈 𝑋 , 𝑦 〉 ∈ 𝐹 ) ) |
8 |
1 7
|
mpbird |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑋 ) = 𝑦 ) |