# Metamath Proof Explorer

## Theorem qliftval

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

Ref Expression
Hypotheses qlift.1 ${⊢}{F}=\mathrm{ran}\left({x}\in {X}⟼⟨\left[{x}\right]{R},{A}⟩\right)$
qlift.2 ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in {Y}$
qlift.3 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
qlift.4 ${⊢}{\phi }\to {X}\in \mathrm{V}$
qliftval.4 ${⊢}{x}={C}\to {A}={B}$
qliftval.6 ${⊢}{\phi }\to \mathrm{Fun}{F}$
Assertion qliftval ${⊢}\left({\phi }\wedge {C}\in {X}\right)\to {F}\left(\left[{C}\right]{R}\right)={B}$

### Proof

Step Hyp Ref Expression
1 qlift.1 ${⊢}{F}=\mathrm{ran}\left({x}\in {X}⟼⟨\left[{x}\right]{R},{A}⟩\right)$
2 qlift.2 ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in {Y}$
3 qlift.3 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
4 qlift.4 ${⊢}{\phi }\to {X}\in \mathrm{V}$
5 qliftval.4 ${⊢}{x}={C}\to {A}={B}$
6 qliftval.6 ${⊢}{\phi }\to \mathrm{Fun}{F}$
7 1 2 3 4 qliftlem ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left[{x}\right]{R}\in \left({X}/{R}\right)$
8 eceq1 ${⊢}{x}={C}\to \left[{x}\right]{R}=\left[{C}\right]{R}$
9 1 7 2 8 5 6 fliftval ${⊢}\left({\phi }\wedge {C}\in {X}\right)\to {F}\left(\left[{C}\right]{R}\right)={B}$