Theorem dff14b

Description: A one-to-one function in terms of different function values for different arguments. (Contributed by Alexander van der Vekens, 26-Jan-2018)

	Ref	Expression
Assertion	dff14b	|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		dff14a	|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) )
2		necom	|- ( x =/= y <-> y =/= x )
3	2	imbi1i	|- ( ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) )
4	3	ralbii	|- ( A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. A ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) )
5		raldifsnb	|- ( A. y e. A ( y =/= x -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
6	4 5	bitri	|- ( A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
7	6	ralbii	|- ( A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) <-> A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
8	7	anbi2i	|- ( ( F : A --> B /\ A. x e. A A. y e. A ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) ) <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )
9	1 8	bitri	|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )