Metamath Proof Explorer
Description: Bound-variable hypothesis builder for a one-to-one function.
(Contributed by NM, 16-May-2004)
|
|
Ref |
Expression |
|
Hypotheses |
nff1.1 |
⊢ Ⅎ 𝑥 𝐹 |
|
|
nff1.2 |
⊢ Ⅎ 𝑥 𝐴 |
|
|
nff1.3 |
⊢ Ⅎ 𝑥 𝐵 |
|
Assertion |
nff1 |
⊢ Ⅎ 𝑥 𝐹 : 𝐴 –1-1→ 𝐵 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nff1.1 |
⊢ Ⅎ 𝑥 𝐹 |
2 |
|
nff1.2 |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
nff1.3 |
⊢ Ⅎ 𝑥 𝐵 |
4 |
|
df-f1 |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ) |
5 |
1 2 3
|
nff |
⊢ Ⅎ 𝑥 𝐹 : 𝐴 ⟶ 𝐵 |
6 |
1
|
nfcnv |
⊢ Ⅎ 𝑥 ◡ 𝐹 |
7 |
6
|
nffun |
⊢ Ⅎ 𝑥 Fun ◡ 𝐹 |
8 |
5 7
|
nfan |
⊢ Ⅎ 𝑥 ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) |
9 |
4 8
|
nfxfr |
⊢ Ⅎ 𝑥 𝐹 : 𝐴 –1-1→ 𝐵 |