Theorem fliftfund

Description: The function F is the unique function defined by FA = B , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	|- F = ran ( x e. X |-> <. A , B >. )
	flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
	flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
	fliftfun.4	|- ( x = y -> A = C )
	fliftfun.5	|- ( x = y -> B = D )
	fliftfund.6	|- ( ( ph /\ ( x e. X /\ y e. X /\ A = C ) ) -> B = D )
Assertion	fliftfund	|- ( ph -> Fun F )

Proof

Step	Hyp	Ref	Expression
1		flift.1	|- F = ran ( x e. X |-> <. A , B >. )
2		flift.2	|- ( ( ph /\ x e. X ) -> A e. R )
3		flift.3	|- ( ( ph /\ x e. X ) -> B e. S )
4		fliftfun.4	|- ( x = y -> A = C )
5		fliftfun.5	|- ( x = y -> B = D )
6		fliftfund.6	|- ( ( ph /\ ( x e. X /\ y e. X /\ A = C ) ) -> B = D )
7	6	3exp2	|- ( ph -> ( x e. X -> ( y e. X -> ( A = C -> B = D ) ) ) )
8	7	imp32	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( A = C -> B = D ) )
9	8	ralrimivva	|- ( ph -> A. x e. X A. y e. X ( A = C -> B = D ) )
10	1 2 3 4 5	fliftfun	|- ( ph -> ( Fun F <-> A. x e. X A. y e. X ( A = C -> B = D ) ) )
11	9 10	mpbird	|- ( ph -> Fun F )