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 ⊢ F Fn A × B → C ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B C = x F y

Proof

Step Hyp Ref Expression
1 fnrnov ⊢ F Fn A × B → ran ⁡ F = z | ∃ x ∈ A ∃ y ∈ B z = x F y
2 1 eleq2d ⊢ F Fn A × B → C ∈ ran ⁡ F ↔ C ∈ z | ∃ x ∈ A ∃ y ∈ B z = x F y
3 ovex ⊢ x F y ∈ V
4 eleq1 ⊢ C = x F y → C ∈ V ↔ x F y ∈ V
5 3 4 mpbiri ⊢ C = x F y → C ∈ V
6 5 rexlimivw ⊢ ∃ y ∈ B C = x F y → C ∈ V
7 6 rexlimivw ⊢ ∃ x ∈ A ∃ y ∈ B C = x F y → C ∈ V
8 eqeq1 ⊢ z = C → z = x F y ↔ C = x F y
9 8 2rexbidv ⊢ z = C → ∃ x ∈ A ∃ y ∈ B z = x F y ↔ ∃ x ∈ A ∃ y ∈ B C = x F y
10 7 9 elab3 ⊢ C ∈ z | ∃ x ∈ A ∃ y ∈ B z = x F y ↔ ∃ x ∈ A ∃ y ∈ B C = x F y
11 2 10 bitrdi ⊢ F Fn A × B → C ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B C = x F y