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 𝑥 𝐹
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𝐵