Theorem fnovrn

Description: An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007)

	Ref	Expression
Assertion	fnovrn	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐹 𝐷 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) )
2		df-ov	⊢ ( 𝐶 𝐹 𝐷 ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝐷 ⟩ )
3		fnfvelrn	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( 𝐹 ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran 𝐹 )
4	2 3	eqeltrid	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( 𝐶 𝐹 𝐷 ) ∈ ran 𝐹 )
5	1 4	sylan2	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐶 𝐹 𝐷 ) ∈ ran 𝐹 )
6	5	3impb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐹 𝐷 ) ∈ ran 𝐹 )