Theorem fmptff

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	fmptff.1	$$⊢\underset{\_}{Ⅎ}xA$$
	fmptff.2	$$⊢\underset{\_}{Ⅎ}xB$$
	fmptff.3	$$⊢F=\left(x\in A⟼C\right)$$
Assertion	fmptff	$$⊢\forall x\in AC\in B\leftrightarrow F:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fmptff.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		fmptff.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		fmptff.3	$$⊢F=\left(x\in A⟼C\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5		nfv	$$⊢ℲyC\in B$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
7	6 2	nfel	$$⊢Ⅎx⦋y/x⦌C\in B$$
8		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
9	8	eleq1d	$$⊢x=y\to \left(C\in B\leftrightarrow ⦋y/x⦌C\in B\right)$$
10	1 4 5 7 9	cbvralfw	$$⊢\forall x\in AC\in B\leftrightarrow \forall y\in A⦋y/x⦌C\in B$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
12	1 4 11 6 8	cbvmptf	$$⊢\left(x\in A⟼C\right)=\left(y\in A⟼⦋y/x⦌C\right)$$
13	3 12	eqtri	$$⊢F=\left(y\in A⟼⦋y/x⦌C\right)$$
14	13	fmpt	$$⊢\forall y\in A⦋y/x⦌C\in B\leftrightarrow F:A⟶B$$
15	10 14	bitri	$$⊢\forall x\in AC\in B\leftrightarrow F:A⟶B$$