Metamath Proof Explorer


Theorem ffnaov

Description: An operation maps to a class to which all values belong, analogous to ffnov . (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion ffnaov ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥𝐴𝑦𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ffnafv ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ) )
2 afveq2 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ''' 𝑤 ) = ( 𝐹 ''' ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-aov (( 𝑥 𝐹 𝑦 )) = ( 𝐹 ''' ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ''' 𝑤 ) = (( 𝑥 𝐹 𝑦 )) )
5 4 eleq1d ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ↔ (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) )
6 5 ralxp ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 )
7 6 anbi2i ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ''' 𝑤 ) ∈ 𝐶 ) ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥𝐴𝑦𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) )
8 1 7 bitri ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥𝐴𝑦𝐵 (( 𝑥 𝐹 𝑦 )) ∈ 𝐶 ) )