Metamath Proof Explorer


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