Theorem fmpodg

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 29-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$$
	fmpodg.3	$$⊢\phi \to R=A\times B$$
Assertion	fmpodg	$$⊢\phi \to F:R⟶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		fmpodg.3	$$⊢\phi \to R=A\times B$$
4	2	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in BC\in S$$
5		eqid	$$⊢\left(x\in A,y\in B⟼C\right)=\left(x\in A,y\in B⟼C\right)$$
6	5	fmpo	$$⊢\forall x\in A\forall y\in BC\in S\leftrightarrow \left(x\in A,y\in B⟼C\right):A\times B⟶S$$
7	4 6	sylib	$$⊢\phi \to \left(x\in A,y\in B⟼C\right):A\times B⟶S$$
8	1 3	feq12d	$$⊢\phi \to \left(F:R⟶S\leftrightarrow \left(x\in A,y\in B⟼C\right):A\times B⟶S\right)$$
9	7 8	mpbird	$$⊢\phi \to F:R⟶S$$