Metamath Proof Explorer

Theorem fvopab6

Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses fvopab6.1 ⊢ F = x y | φ ∧ y = B
fvopab6.2 ⊢ x = A → φ ↔ ψ
fvopab6.3 ⊢ x = A → B = C
Assertion fvopab6 ⊢ A ∈ D ∧ C ∈ R ∧ ψ → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvopab6.1 ⊢ F = x y | φ ∧ y = B
2 fvopab6.2 ⊢ x = A → φ ↔ ψ
3 fvopab6.3 ⊢ x = A → B = C
4 elex ⊢ A ∈ D → A ∈ V
5 3 eqeq2d ⊢ x = A → y = B ↔ y = C
6 2 5 anbi12d ⊢ x = A → φ ∧ y = B ↔ ψ ∧ y = C
7 iba ⊢ y = C → ψ ↔ ψ ∧ y = C
8 7 bicomd ⊢ y = C → ψ ∧ y = C ↔ ψ
9 moeq ⊢ ∃* y y = B
10 9 moani ⊢ ∃* y φ ∧ y = B
11 10 a1i ⊢ x ∈ V → ∃* y φ ∧ y = B
12 vex ⊢ x ∈ V
13 12 biantrur ⊢ φ ∧ y = B ↔ x ∈ V ∧ φ ∧ y = B
14 13 opabbii ⊢ x y | φ ∧ y = B = x y | x ∈ V ∧ φ ∧ y = B
15 1 14 eqtri ⊢ F = x y | x ∈ V ∧ φ ∧ y = B
16 6 8 11 15 fvopab3ig ⊢ A ∈ V ∧ C ∈ R → ψ → F ⁡ A = C
17 4 16 sylan ⊢ A ∈ D ∧ C ∈ R → ψ → F ⁡ A = C
18 17 3impia ⊢ A ∈ D ∧ C ∈ R ∧ ψ → F ⁡ A = C