Theorem fovcl

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007) (Proof shortened by AV, 9-Mar-2025)

	Ref	Expression
Hypothesis	fovcl.1	⊢ 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶
Assertion	fovcl	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fovcl.1	⊢ 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶
2	1	a1i	⊢ ( 𝐴 ∈ 𝑅 → 𝐹 : ( 𝑅 × 𝑆 ) ⟶ 𝐶 )
3	2	fovcld	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )
4	3	3anidm12	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝐶 )