Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Probability
Preimage set mapping operator
elorvc
Next ⟩
orvcval4
Metamath Proof Explorer
Ascii
Unicode
Theorem
elorvc
Description:
Elementhood of a preimage.
(Contributed by
Thierry Arnoux
, 21-Jan-2017)
Ref
Expression
Hypotheses
orvcval.1
⊢
φ
→
Fun
⁡
X
orvcval.2
⊢
φ
→
X
∈
V
orvcval.3
⊢
φ
→
A
∈
W
Assertion
elorvc
⊢
φ
∧
z
∈
dom
⁡
X
→
z
∈
X
R
RV/c
A
↔
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
orvcval2
⊢
φ
→
X
R
RV/c
A
=
z
∈
dom
⁡
X
|
X
⁡
z
R
A
5
4
eleq2d
⊢
φ
→
z
∈
X
R
RV/c
A
↔
z
∈
z
∈
dom
⁡
X
|
X
⁡
z
R
A
6
rabid
⊢
z
∈
z
∈
dom
⁡
X
|
X
⁡
z
R
A
↔
z
∈
dom
⁡
X
∧
X
⁡
z
R
A
7
5
6
syl6bb
⊢
φ
→
z
∈
X
R
RV/c
A
↔
z
∈
dom
⁡
X
∧
X
⁡
z
R
A
8
7
baibd
⊢
φ
∧
z
∈
dom
⁡
X
→
z
∈
X
R
RV/c
A
↔
X
⁡
z
R
A