Theorem fmptff

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

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

Proof

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