Metamath Proof Explorer

Theorem fvopab3ig

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999)

Ref Expression
Hypotheses fvopab3ig.1 ⊢x=A→φ↔ψ
fvopab3ig.2 ⊢y=B→ψ↔χ
fvopab3ig.3 ⊢x∈C→∃*yφ
fvopab3ig.4 ⊢F=xy|x∈C∧φ
Assertion fvopab3ig ⊢A∈C∧B∈D→χ→F⁡A=B

Proof

Step Hyp Ref Expression
1 fvopab3ig.1 ⊢x=A→φ↔ψ
2 fvopab3ig.2 ⊢y=B→ψ↔χ
3 fvopab3ig.3 ⊢x∈C→∃*yφ
4 fvopab3ig.4 ⊢F=xy|x∈C∧φ
5 eleq1 ⊢x=A→x∈C↔A∈C
6 5 1 anbi12d ⊢x=A→x∈C∧φ↔A∈C∧ψ
7 2 anbi2d ⊢y=B→A∈C∧ψ↔A∈C∧χ
8 6 7 opelopabg ⊢A∈C∧B∈D→AB∈xy|x∈C∧φ↔A∈C∧χ
9 8 biimpar ⊢A∈C∧B∈D∧A∈C∧χ→AB∈xy|x∈C∧φ
10 9 exp43 ⊢A∈C→B∈D→A∈C→χ→AB∈xy|x∈C∧φ
11 10 pm2.43a ⊢A∈C→B∈D→χ→AB∈xy|x∈C∧φ
12 11 imp ⊢A∈C∧B∈D→χ→AB∈xy|x∈C∧φ
13 4 fveq1i ⊢F⁡A=xy|x∈C∧φ⁡A
14 funopab ⊢Fun⁡xy|x∈C∧φ↔∀x∃*yx∈C∧φ
15 moanimv ⊢∃*yx∈C∧φ↔x∈C→∃*yφ
16 3 15 mpbir ⊢∃*yx∈C∧φ
17 14 16 mpgbir ⊢Fun⁡xy|x∈C∧φ
18 funopfv ⊢Fun⁡xy|x∈C∧φ→AB∈xy|x∈C∧φ→xy|x∈C∧φ⁡A=B
19 17 18 ax-mp ⊢AB∈xy|x∈C∧φ→xy|x∈C∧φ⁡A=B
20 13 19 eqtrid ⊢AB∈xy|x∈C∧φ→F⁡A=B
21 12 20 syl6 ⊢A∈C∧B∈D→χ→F⁡A=B