Metamath Proof Explorer


Theorem fvopab3g

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypotheses fvopab3g.2 x = A φ ψ
fvopab3g.3 y = B ψ χ
fvopab3g.4 x C ∃! y φ
fvopab3g.5 F = x y | x C φ
Assertion fvopab3g A C B D F A = B χ

Proof

Step Hyp Ref Expression
1 fvopab3g.2 x = A φ ψ
2 fvopab3g.3 y = B ψ χ
3 fvopab3g.4 x C ∃! y φ
4 fvopab3g.5 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 3 4 fnopab F Fn C
10 fnopfvb F Fn C A C F A = B A B F
11 9 10 mpan A C F A = B A B F
12 4 eleq2i A B F A B x y | x C φ
13 11 12 bitrdi A C F A = B A B x y | x C φ
14 13 adantr A C B D F A = B A B x y | x C φ
15 ibar A C χ A C χ
16 15 adantr A C B D χ A C χ
17 8 14 16 3bitr4d A C B D F A = B χ