Theorem fnmptif

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	fnmptif.1	⊢ Ⅎ 𝑥 𝐴
	fnmptif.2	⊢ 𝐵 ∈ V
	fnmptif.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fnmptif	⊢ 𝐹 Fn 𝐴

Proof

Step	Hyp	Ref	Expression
1		fnmptif.1	⊢ Ⅎ 𝑥 𝐴
2		fnmptif.2	⊢ 𝐵 ∈ V
3		fnmptif.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V
5	1	mptfnf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
6	4 5	mpbi	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴
7	3	fneq1i	⊢ ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
8	6 7	mpbir	⊢ 𝐹 Fn 𝐴