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

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 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) }
fvopab6.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
fvopab6.3 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion fvopab6 ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fvopab6.1 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) }
2 fvopab6.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 fvopab6.3 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4 elex ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ V )
5 3 eqeq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐶 ) )
6 2 5 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑦 = 𝐵 ) ↔ ( 𝜓 ∧ 𝑦 = 𝐶 ) ) )
7 iba ⊢ ( 𝑦 = 𝐶 → ( 𝜓 ↔ ( 𝜓 ∧ 𝑦 = 𝐶 ) ) )
8 7 bicomd ⊢ ( 𝑦 = 𝐶 → ( ( 𝜓 ∧ 𝑦 = 𝐶 ) ↔ 𝜓 ) )
9 moeq ⊢ ∃* 𝑦 𝑦 = 𝐵
10 9 moani ⊢ ∃* 𝑦 ( 𝜑 ∧ 𝑦 = 𝐵 )
11 10 a1i ⊢ ( 𝑥 ∈ V → ∃* 𝑦 ( 𝜑 ∧ 𝑦 = 𝐵 ) )
12 vex ⊢ 𝑥 ∈ V
13 12 biantrur ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) )
14 13 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) }
15 1 14 eqtri ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ ( 𝜑 ∧ 𝑦 = 𝐵 ) ) }
16 6 8 11 15 fvopab3ig ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑅 ) → ( 𝜓 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
17 4 16 sylan ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ) → ( 𝜓 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) )
18 17 3impia ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )