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 φPProb
dstrvprob.2 φXRndVarP
orvcelel.1 φA𝔅
Assertion orvcelval φXERV/cA=X-1A

Proof

Step Hyp Ref Expression
1 dstrvprob.1 φPProb
2 dstrvprob.2 φXRndVarP
3 orvcelel.1 φA𝔅
4 1 2 3 orrvcval4 φXERV/cA=X-1x|xEA
5 epelg A𝔅xEAxA
6 3 5 syl φxEAxA
7 6 rabbidv φx|xEA=x|xA
8 dfin5 A=x|xA
9 8 a1i φA=x|xA
10 elssuni A𝔅A𝔅
11 unibrsiga 𝔅=
12 10 11 sseqtrdi A𝔅A
13 3 12 syl φA
14 sseqin2 AA=A
15 13 14 sylib φA=A
16 7 9 15 3eqtr2d φx|xEA=A
17 16 imaeq2d φX-1x|xEA=X-1A
18 4 17 eqtrd φXERV/cA=X-1A