Theorem ovelrn

Description: A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 30-Jan-2014)

	Ref	Expression
Assertion	ovelrn	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnov	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) } )
2	1	eleq2d	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ( 𝐶 ∈ ran 𝐹 ↔ 𝐶 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) } ) )
3		ovex	⊢ ( 𝑥 𝐹 𝑦 ) ∈ V
4		eleq1	⊢ ( 𝐶 = ( 𝑥 𝐹 𝑦 ) → ( 𝐶 ∈ V ↔ ( 𝑥 𝐹 𝑦 ) ∈ V ) )
5	3 4	mpbiri	⊢ ( 𝐶 = ( 𝑥 𝐹 𝑦 ) → 𝐶 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) → 𝐶 ∈ V )
7	6	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) → 𝐶 ∈ V )
8		eqeq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 = ( 𝑥 𝐹 𝑦 ) ↔ 𝐶 = ( 𝑥 𝐹 𝑦 ) ) )
9	8	2rexbidv	⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) ) )
10	7 9	elab3	⊢ ( 𝐶 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) )
11	2 10	bitrdi	⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) ) )