This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffnfvf

Description: A function maps to a class to which all values belong. This version of ffnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypotheses ffnfvf.1 
|- F/_ x A
ffnfvf.2 
|- F/_ x B
ffnfvf.3 
|- F/_ x F
Assertion ffnfvf 
|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 ffnfvf.1 
 |-  F/_ x A
2 ffnfvf.2 
 |-  F/_ x B
3 ffnfvf.3 
 |-  F/_ x F
4 ffnfv 
 |-  ( F : A --> B <-> ( F Fn A /\ A. z e. A ( F ` z ) e. B ) )
5 nfcv 
 |-  F/_ z A
6 nfcv 
 |-  F/_ x z
7 3 6 nffv 
 |-  F/_ x ( F ` z )
8 7 2 nfel 
 |-  F/ x ( F ` z ) e. B
9 nfv 
 |-  F/ z ( F ` x ) e. B
10 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
11 10 eleq1d 
 |-  ( z = x -> ( ( F ` z ) e. B <-> ( F ` x ) e. B ) )
12 5 1 8 9 11 cbvralfw 
 |-  ( A. z e. A ( F ` z ) e. B <-> A. x e. A ( F ` x ) e. B )
13 12 anbi2i 
 |-  ( ( F Fn A /\ A. z e. A ( F ` z ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
14 4 13 bitri 
 |-  ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )