Theorem qliftel1

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	qliftel1	|- ( ( ph /\ x e. X ) -> [ x ] R F 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	fliftel1	|- ( ( ph /\ x e. X ) -> [ x ] R F A )