Metamath Proof Explorer


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 )