Metamath Proof Explorer


Theorem fliftval

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

Ref Expression
Hypotheses flift.1 F=ranxXAB
flift.2 φxXAR
flift.3 φxXBS
fliftval.4 x=YA=C
fliftval.5 x=YB=D
fliftval.6 φFunF
Assertion fliftval φYXFC=D

Proof

Step Hyp Ref Expression
1 flift.1 F=ranxXAB
2 flift.2 φxXAR
3 flift.3 φxXBS
4 fliftval.4 x=YA=C
5 fliftval.5 x=YB=D
6 fliftval.6 φFunF
7 6 adantr φYXFunF
8 simpr φYXYX
9 eqidd φD=D
10 eqidd YXC=C
11 9 10 anim12ci φYXC=CD=D
12 4 eqeq2d x=YC=AC=C
13 5 eqeq2d x=YD=BD=D
14 12 13 anbi12d x=YC=AD=BC=CD=D
15 14 rspcev YXC=CD=DxXC=AD=B
16 8 11 15 syl2anc φYXxXC=AD=B
17 1 2 3 fliftel φCFDxXC=AD=B
18 17 adantr φYXCFDxXC=AD=B
19 16 18 mpbird φYXCFD
20 funbrfv FunFCFDFC=D
21 7 19 20 sylc φYXFC=D