Metamath Proof Explorer


Theorem orvcval2

Description: Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017)

Ref Expression
Hypotheses orvcval.1 φ Fun X
orvcval.2 φ X V
orvcval.3 φ A W
Assertion orvcval2 φ X R RV/c A = z dom X | X z R A

Proof

Step Hyp Ref Expression
1 orvcval.1 φ Fun X
2 orvcval.2 φ X V
3 orvcval.3 φ A W
4 1 2 3 orvcval φ X R RV/c A = X -1 y | y R A
5 funfn Fun X X Fn dom X
6 1 5 sylib φ X Fn dom X
7 fncnvima2 X Fn dom X X -1 y | y R A = z dom X | X z y | y R A
8 6 7 syl φ X -1 y | y R A = z dom X | X z y | y R A
9 fvex X z V
10 breq1 y = X z y R A X z R A
11 9 10 elab X z y | y R A X z R A
12 11 rabbii z dom X | X z y | y R A = z dom X | X z R A
13 12 a1i φ z dom X | X z y | y R A = z dom X | X z R A
14 4 8 13 3eqtrd φ X R RV/c A = z dom X | X z R A