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 = x y | 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 = x y | 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 A B x y | x C φ A C χ
9 8 biimpar A C B D A C χ A B x y | x C φ
10 9 exp43 A C B D A C χ A B x y | x C φ
11 10 pm2.43a A C B D χ A B x y | x C φ
12 11 imp A C B D χ A B x y | x C φ
13 4 fveq1i F A = x y | x C φ A
14 funopab Fun x y | x C φ x * y x C φ
15 moanimv * y x C φ x C * y φ
16 3 15 mpbir * y x C φ
17 14 16 mpgbir Fun x y | x C φ
18 funopfv Fun x y | x C φ A B x y | x C φ x y | x C φ A = B
19 17 18 ax-mp A B x y | x C φ x y | x C φ A = B
20 13 19 eqtrid A B x y | x C φ F A = B
21 12 20 syl6 A C B D χ F A = B