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	$$⊢F:R\times S⟶C$$
Assertion	fovcl	$$⊢\left(A\in R\wedge B\in S\right)\to AFB\in C$$

Proof

Step	Hyp	Ref	Expression
1		fovcl.1	$$⊢F:R\times S⟶C$$
2	1	a1i	$$⊢A\in R\to F:R\times S⟶C$$
3	2	fovcld	$$⊢\left(A\in R\wedge A\in R\wedge B\in S\right)\to AFB\in C$$
4	3	3anidm12	$$⊢\left(A\in R\wedge B\in S\right)\to AFB\in C$$