Metamath Proof Explorer


Theorem eldmcnv

Description: Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018)

Ref Expression
Assertion eldmcnv AVAdomR-1uuRA

Proof

Step Hyp Ref Expression
1 eldmg AVAdomR-1uAR-1u
2 brcnvg AVuVAR-1uuRA
3 2 elvd AVAR-1uuRA
4 3 exbidv AVuAR-1uuuRA
5 1 4 bitrd AVAdomR-1uuRA