Metamath Proof Explorer


Theorem eldm4

Description: Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018)

Ref Expression
Assertion eldm4 AVAdomRyyAR

Proof

Step Hyp Ref Expression
1 eldmg AVAdomRyARy
2 elecALTV AVyVyARARy
3 2 elvd AVyARARy
4 3 exbidv AVyyARyARy
5 1 4 bitr4d AVAdomRyyAR