Metamath Proof Explorer


Theorem qliftval

Description: The value of the function F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

Ref Expression
Hypotheses qlift.1 F = ran x X x R A
qlift.2 φ x X A Y
qlift.3 φ R Er X
qlift.4 φ X V
qliftval.4 x = C A = B
qliftval.6 φ Fun F
Assertion qliftval φ C X F C R = B

Proof

Step Hyp Ref Expression
1 qlift.1 F = ran x X x R A
2 qlift.2 φ x X A Y
3 qlift.3 φ R Er X
4 qlift.4 φ X V
5 qliftval.4 x = C A = B
6 qliftval.6 φ Fun F
7 1 2 3 4 qliftlem φ x X x R X / R
8 eceq1 x = C x R = C R
9 1 7 2 8 5 6 fliftval φ C X F C R = B