| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-br 5143 | . . . . 5
⊢
(〈𝐴, 𝐵〉uncurry 𝐹𝑤 ↔ 〈〈𝐴, 𝐵〉, 𝑤〉 ∈ uncurry 𝐹) | 
| 2 |  | df-unc 8294 | . . . . . 6
⊢ uncurry
𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} | 
| 3 | 2 | eleq2i 2832 | . . . . 5
⊢
(〈〈𝐴,
𝐵〉, 𝑤〉 ∈ uncurry 𝐹 ↔ 〈〈𝐴, 𝐵〉, 𝑤〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧}) | 
| 4 | 1, 3 | bitri 275 | . . . 4
⊢
(〈𝐴, 𝐵〉uncurry 𝐹𝑤 ↔ 〈〈𝐴, 𝐵〉, 𝑤〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧}) | 
| 5 |  | vex 3483 | . . . . 5
⊢ 𝑤 ∈ V | 
| 6 |  | simp2 1137 | . . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝑤) → 𝑦 = 𝐵) | 
| 7 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝑤) → (𝐹‘𝑥) = (𝐹‘𝐴)) | 
| 9 |  | simp3 1138 | . . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝑤) → 𝑧 = 𝑤) | 
| 10 | 6, 8, 9 | breq123d 5156 | . . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝑤) → (𝑦(𝐹‘𝑥)𝑧 ↔ 𝐵(𝐹‘𝐴)𝑤)) | 
| 11 | 10 | eloprabga 7543 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑤 ∈ V) → (〈〈𝐴, 𝐵〉, 𝑤〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} ↔ 𝐵(𝐹‘𝐴)𝑤)) | 
| 12 | 5, 11 | mp3an3 1451 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈〈𝐴, 𝐵〉, 𝑤〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} ↔ 𝐵(𝐹‘𝐴)𝑤)) | 
| 13 | 4, 12 | bitrid 283 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉uncurry 𝐹𝑤 ↔ 𝐵(𝐹‘𝐴)𝑤)) | 
| 14 | 13 | iotabidv 6544 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (℩𝑤〈𝐴, 𝐵〉uncurry 𝐹𝑤) = (℩𝑤𝐵(𝐹‘𝐴)𝑤)) | 
| 15 |  | df-ov 7435 | . . 3
⊢ (𝐴uncurry 𝐹𝐵) = (uncurry 𝐹‘〈𝐴, 𝐵〉) | 
| 16 |  | df-fv 6568 | . . 3
⊢ (uncurry
𝐹‘〈𝐴, 𝐵〉) = (℩𝑤〈𝐴, 𝐵〉uncurry 𝐹𝑤) | 
| 17 | 15, 16 | eqtri 2764 | . 2
⊢ (𝐴uncurry 𝐹𝐵) = (℩𝑤〈𝐴, 𝐵〉uncurry 𝐹𝑤) | 
| 18 |  | df-fv 6568 | . 2
⊢ ((𝐹‘𝐴)‘𝐵) = (℩𝑤𝐵(𝐹‘𝐴)𝑤) | 
| 19 | 14, 17, 18 | 3eqtr4g 2801 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) |