Theorem nfmpo

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

	Ref	Expression
Hypotheses	nfmpo.1	⊢ Ⅎ 𝑧 𝐴
	nfmpo.2	⊢ Ⅎ 𝑧 𝐵
	nfmpo.3	⊢ Ⅎ 𝑧 𝐶
Assertion	nfmpo	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		nfmpo.1	⊢ Ⅎ 𝑧 𝐴
2		nfmpo.2	⊢ Ⅎ 𝑧 𝐵
3		nfmpo.3	⊢ Ⅎ 𝑧 𝐶
4		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) }
5	1	nfcri	⊢ Ⅎ 𝑧 𝑥 ∈ 𝐴
6	2	nfcri	⊢ Ⅎ 𝑧 𝑦 ∈ 𝐵
7	5 6	nfan	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
8	3	nfeq2	⊢ Ⅎ 𝑧 𝑤 = 𝐶
9	7 8	nfan	⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 )
10	9	nfoprab	⊢ Ⅎ 𝑧 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) }
11	4 10	nfcxfr	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )