Theorem qliftfund

Description: The function F is the unique function defined by F[ x ] = A , provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

	Ref	Expression
Hypotheses	qlift.1	|- F = ran ( x e. X |-> <. [ x ] R , A >. )
	qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
	qlift.3	|- ( ph -> R Er X )
	qlift.4	|- ( ph -> X e. V )
	qliftfun.4	|- ( x = y -> A = B )
	qliftfund.6	|- ( ( ph /\ x R y ) -> A = B )
Assertion	qliftfund	|- ( ph -> Fun F )

Proof

Step	Hyp	Ref	Expression
1		qlift.1	|- F = ran ( x e. X |-> <. [ x ] R , A >. )
2		qlift.2	|- ( ( ph /\ x e. X ) -> A e. Y )
3		qlift.3	|- ( ph -> R Er X )
4		qlift.4	|- ( ph -> X e. V )
5		qliftfun.4	|- ( x = y -> A = B )
6		qliftfund.6	|- ( ( ph /\ x R y ) -> A = B )
7	6	ex	|- ( ph -> ( x R y -> A = B ) )
8	7	alrimivv	|- ( ph -> A. x A. y ( x R y -> A = B ) )
9	1 2 3 4 5	qliftfun	|- ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )
10	8 9	mpbird	|- ( ph -> Fun F )