Metamath Proof Explorer


Theorem orvcelval

Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017)

Ref Expression
Hypotheses dstrvprob.1 φ P Prob
dstrvprob.2 φ X RndVar P
orvcelel.1 φ A 𝔅
Assertion orvcelval φ X E RV/c A = X -1 A

Proof

Step Hyp Ref Expression
1 dstrvprob.1 φ P Prob
2 dstrvprob.2 φ X RndVar P
3 orvcelel.1 φ A 𝔅
4 1 2 3 orrvcval4 φ X E RV/c A = X -1 x | x E A
5 epelg A 𝔅 x E A x A
6 3 5 syl φ x E A x A
7 6 rabbidv φ x | x E A = x | x A
8 dfin5 A = x | x A
9 8 a1i φ A = x | x A
10 elssuni A 𝔅 A 𝔅
11 unibrsiga 𝔅 =
12 10 11 sseqtrdi A 𝔅 A
13 3 12 syl φ A
14 sseqin2 A A = A
15 13 14 sylib φ A = A
16 7 9 15 3eqtr2d φ x | x E A = A
17 16 imaeq2d φ X -1 x | x E A = X -1 A
18 4 17 eqtrd φ X E RV/c A = X -1 A