Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
eldmcnv
Next ⟩
dfrel5
Metamath Proof Explorer
Ascii
Unicode
Theorem
eldmcnv
Description:
Elementhood in a domain of a converse.
(Contributed by
Peter Mazsa
, 25-May-2018)
Ref
Expression
Assertion
eldmcnv
⊢
A
∈
V
→
A
∈
dom
⁡
R
-1
↔
∃
u
u
R
A
Proof
Step
Hyp
Ref
Expression
1
eldmg
⊢
A
∈
V
→
A
∈
dom
⁡
R
-1
↔
∃
u
A
R
-1
u
2
brcnvg
⊢
A
∈
V
∧
u
∈
V
→
A
R
-1
u
↔
u
R
A
3
2
elvd
⊢
A
∈
V
→
A
R
-1
u
↔
u
R
A
4
3
exbidv
⊢
A
∈
V
→
∃
u
A
R
-1
u
↔
∃
u
u
R
A
5
1
4
bitrd
⊢
A
∈
V
→
A
∈
dom
⁡
R
-1
↔
∃
u
u
R
A