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 | ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↦ 𝐵 ) |
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 | ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ↦ 𝐵 ) |