Metamath Proof Explorer


Theorem funimassov

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013)

Ref Expression
Assertion funimassov ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 funimass4 ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹𝑧 ) ∈ 𝐶 ) )
2 fveq2 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹𝑧 ) = ( 𝑥 𝐹 𝑦 ) )
5 4 eleq1d ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹𝑧 ) ∈ 𝐶 ↔ ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )
6 5 ralxp ( ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹𝑧 ) ∈ 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 )
7 1 6 bitrdi ( ( Fun 𝐹 ∧ ( 𝐴 × 𝐵 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐴 × 𝐵 ) ) ⊆ 𝐶 ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) )