Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
eldmres
Next ⟩
eldm4
Metamath Proof Explorer
Ascii
Unicode
Theorem
eldmres
Description:
Elementhood in the domain of a restriction.
(Contributed by
Peter Mazsa
, 9-Jan-2019)
Ref
Expression
Assertion
eldmres
⊢
B
∈
V
→
B
∈
dom
⁡
R
↾
A
↔
B
∈
A
∧
∃
y
B
R
y
Proof
Step
Hyp
Ref
Expression
1
eldmg
⊢
B
∈
V
→
B
∈
dom
⁡
R
↾
A
↔
∃
y
B
R
↾
A
y
2
brres
⊢
y
∈
V
→
B
R
↾
A
y
↔
B
∈
A
∧
B
R
y
3
2
elv
⊢
B
R
↾
A
y
↔
B
∈
A
∧
B
R
y
4
3
exbii
⊢
∃
y
B
R
↾
A
y
↔
∃
y
B
∈
A
∧
B
R
y
5
19.42v
⊢
∃
y
B
∈
A
∧
B
R
y
↔
B
∈
A
∧
∃
y
B
R
y
6
4
5
bitri
⊢
∃
y
B
R
↾
A
y
↔
B
∈
A
∧
∃
y
B
R
y
7
1
6
bitrdi
⊢
B
∈
V
→
B
∈
dom
⁡
R
↾
A
↔
B
∈
A
∧
∃
y
B
R
y