Theorem nfmpt

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

	Ref	Expression
Hypotheses	nfmpt.1	⊢ Ⅎ 𝑥 𝐴
	nfmpt.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfmpt	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfmpt.1	⊢ Ⅎ 𝑥 𝐴
2		nfmpt.2	⊢ Ⅎ 𝑥 𝐵
3		df-mpt	⊢ ( 𝑦 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) }
4	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5	2	nfeq2	⊢ Ⅎ 𝑥 𝑧 = 𝐵
6	4 5	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵 )
7	6	nfopab	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) }
8	3 7	nfcxfr	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↦ 𝐵 )