Theorem fmptf

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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