Metamath Proof Explorer


Theorem refrelcosslem

Description: Lemma for the left side of the refrelcoss3 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019)

Ref Expression
Assertion refrelcosslem x dom R x R x

Proof

Step Hyp Ref Expression
1 ralel x dom R x dom R
2 eldmcoss2 x V x dom R x R x
3 2 elv x dom R x R x
4 3 ralbii x dom R x dom R x dom R x R x
5 1 4 mpbi x dom R x R x