Metamath Proof Explorer


Theorem nffo

Description: Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004)

Ref Expression
Hypotheses nffo.1 _xF
nffo.2 _xA
nffo.3 _xB
Assertion nffo xF:AontoB

Proof

Step Hyp Ref Expression
1 nffo.1 _xF
2 nffo.2 _xA
3 nffo.3 _xB
4 df-fo F:AontoBFFnAranF=B
5 1 2 nffn xFFnA
6 1 nfrn _xranF
7 6 3 nfeq xranF=B
8 5 7 nfan xFFnAranF=B
9 4 8 nfxfr xF:AontoB