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 syl5eq ⊢ A B ∈ x y | x ∈ C ∧ φ → F ⁡ A = B
21 12 20 syl6 ⊢ A ∈ C ∧ B ∈ D → χ → F ⁡ A = B