Metamath Proof Explorer
Description: Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004)
|
|
Ref |
Expression |
|
Hypotheses |
nffo.1 |
|
|
|
nffo.2 |
|
|
|
nffo.3 |
|
|
Assertion |
nffo |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nffo.1 |
|
2 |
|
nffo.2 |
|
3 |
|
nffo.3 |
|
4 |
|
df-fo |
|
5 |
1 2
|
nffn |
|
6 |
1
|
nfrn |
|
7 |
6 3
|
nfeq |
|
8 |
5 7
|
nfan |
|
9 |
4 8
|
nfxfr |
|