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=ranxXxRA
qlift.2 φxXAY
qlift.3 φRErX
qlift.4 φXV
Assertion qliftel1 φxXxRFA

Proof

Step Hyp Ref Expression
1 qlift.1 F=ranxXxRA
2 qlift.2 φxXAY
3 qlift.3 φRErX
4 qlift.4 φXV
5 1 2 3 4 qliftlem φxXxRX/R
6 1 5 2 fliftel1 φxXxRFA