Theorem fmptf

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

	Ref	Expression
Hypotheses	fmptf.1	⊢ Ⅎ 𝑥 𝐵
	fmptf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion	fmptf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fmptf.1	⊢ Ⅎ 𝑥 𝐵
2		fmptf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		nfv	⊢ Ⅎ 𝑦 𝐶 ∈ 𝐵
4		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
5	4 1	nfel	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵
6		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
7	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) )
8	3 5 7	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 )
9		nfcv	⊢ Ⅎ 𝑦 𝐶
10	9 4 6	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
11	2 10	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12	11	fmpt	⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
13	8 12	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )