Theorem fnrnov

Description: The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006)

	Ref	Expression
Assertion	fnrnov	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ran 𝐹 = { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) } )
2		fveq2	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4	2 3	eqtr4di	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝑥 𝐹 𝑦 ) )
5	4	eqeq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
6	5	rexxp	⊢ ( ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) )
7	6	abbii	⊢ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) }
8	1 7	eqtrdi	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) } )