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