Step |
Hyp |
Ref |
Expression |
1 |
|
ovidig.1 |
⊢ ∃* 𝑧 𝜑 |
2 |
|
ovidig.2 |
⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } |
3 |
|
df-ov |
⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) |
4 |
1
|
funoprab |
⊢ Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } |
5 |
2
|
funeqi |
⊢ ( Fun 𝐹 ↔ Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } ) |
6 |
4 5
|
mpbir |
⊢ Fun 𝐹 |
7 |
|
oprabidw |
⊢ ( 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } ↔ 𝜑 ) |
8 |
7
|
biimpri |
⊢ ( 𝜑 → 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∈ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝜑 } ) |
9 |
8 2
|
eleqtrrdi |
⊢ ( 𝜑 → 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∈ 𝐹 ) |
10 |
|
funopfv |
⊢ ( Fun 𝐹 → ( 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∈ 𝐹 → ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) = 𝑧 ) ) |
11 |
6 9 10
|
mpsyl |
⊢ ( 𝜑 → ( 𝐹 ‘ 〈 𝑥 , 𝑦 〉 ) = 𝑧 ) |
12 |
3 11
|
eqtrid |
⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) |