Metamath Proof Explorer


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 𝐹 ↔ ∃ 𝑥𝐴𝑦𝐵 𝐶 = ( 𝑥 𝐹 𝑦 ) ) )