Theorem qliftel

Description: Elementhood in the relation F . (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 )
Assertion	qliftel	|- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )

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	1 2 3 4	qliftlem	|- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
6	1 5 2	fliftel	|- ( ph -> ( [ C ] R F D <-> E. x e. X ( [ C ] R = [ x ] R /\ D = A ) ) )
7	3	adantr	|- ( ( ph /\ x e. X ) -> R Er X )
8		simpr	|- ( ( ph /\ x e. X ) -> x e. X )
9	7 8	erth2	|- ( ( ph /\ x e. X ) -> ( C R x <-> [ C ] R = [ x ] R ) )
10	9	anbi1d	|- ( ( ph /\ x e. X ) -> ( ( C R x /\ D = A ) <-> ( [ C ] R = [ x ] R /\ D = A ) ) )
11	10	rexbidva	|- ( ph -> ( E. x e. X ( C R x /\ D = A ) <-> E. x e. X ( [ C ] R = [ x ] R /\ D = A ) ) )
12	6 11	bitr4d	|- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )