This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↔ χ