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 𝐴 ∧ ( 𝐵 × 𝐶 ) ⊆ 𝐴 ) → ( 𝐷 ∈ ( 𝐹 “ ( 𝐵 × 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 𝐷 = ( 𝑥 𝐹 𝑦 ) ) )