Description: Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nff1.1 | |- F/_ x F |
|
nff1.2 | |- F/_ x A |
||
nff1.3 | |- F/_ x B |
||
Assertion | nff1 | |- F/ x F : A -1-1-> B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nff1.1 | |- F/_ x F |
|
2 | nff1.2 | |- F/_ x A |
|
3 | nff1.3 | |- F/_ x B |
|
4 | df-f1 | |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) ) |
|
5 | 1 2 3 | nff | |- F/ x F : A --> B |
6 | 1 | nfcnv | |- F/_ x `' F |
7 | 6 | nffun | |- F/ x Fun `' F |
8 | 5 7 | nfan | |- F/ x ( F : A --> B /\ Fun `' F ) |
9 | 4 8 | nfxfr | |- F/ x F : A -1-1-> B |