Metamath Proof Explorer
Theorem nff
Description: Bound-variable hypothesis builder for a mapping. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)
|
|
Ref |
Expression |
|
Hypotheses |
nff.1 |
⊢ Ⅎ 𝑥 𝐹 |
|
|
nff.2 |
⊢ Ⅎ 𝑥 𝐴 |
|
|
nff.3 |
⊢ Ⅎ 𝑥 𝐵 |
|
Assertion |
nff |
⊢ Ⅎ 𝑥 𝐹 : 𝐴 ⟶ 𝐵 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nff.1 |
⊢ Ⅎ 𝑥 𝐹 |
2 |
|
nff.2 |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
nff.3 |
⊢ Ⅎ 𝑥 𝐵 |
4 |
|
df-f |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ) |
5 |
1 2
|
nffn |
⊢ Ⅎ 𝑥 𝐹 Fn 𝐴 |
6 |
1
|
nfrn |
⊢ Ⅎ 𝑥 ran 𝐹 |
7 |
6 3
|
nfss |
⊢ Ⅎ 𝑥 ran 𝐹 ⊆ 𝐵 |
8 |
5 7
|
nfan |
⊢ Ⅎ 𝑥 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) |
9 |
4 8
|
nfxfr |
⊢ Ⅎ 𝑥 𝐹 : 𝐴 ⟶ 𝐵 |