Theorem fmpod

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fmpodg.1	$$⊢\phi \to F=\left(x\in A,y\in B⟼C\right)$$
	fmpodg.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to C\in S$$
Assertion	fmpod	$$⊢\phi \to F:A\times B⟶S$$

Proof

Step	Hyp	Ref	Expression
1		fmpodg.1	$$⊢\phi \to F=\left(x\in A,y\in B⟼C\right)$$
2		fmpodg.2	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to C\in S$$
3		eqidd	$$⊢\phi \to A\times B=A\times B$$
4	1 2 3	fmpodg	$$⊢\phi \to F:A\times B⟶S$$