Metamath Proof Explorer


Theorem nff1

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

Proof

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