Metamath Proof Explorer


Theorem ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion ovelimab ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥𝐵𝑦𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 fvelimab ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) ( 𝐹𝑧 ) = 𝐷 ) )
2 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5 4 eqeq1d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹𝑧 ) = 𝐷 ↔ ( 𝑥 𝐹 𝑦 ) = 𝐷 ) )
6 eqcom ( ( 𝑥 𝐹 𝑦 ) = 𝐷𝐷 = ( 𝑥 𝐹 𝑦 ) )
7 5 6 bitrdi ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹𝑧 ) = 𝐷𝐷 = ( 𝑥 𝐹 𝑦 ) ) )
8 7 rexxp ( ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) ( 𝐹𝑧 ) = 𝐷 ↔ ∃ 𝑥𝐵𝑦𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) )
9 1 8 bitrdi ( ( 𝐹 Fn 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥𝐵𝑦𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )