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 xdomRxRx

Proof

Step Hyp Ref Expression
1 ralel xdomRxdomR
2 eldmcoss2 xVxdomRxRx
3 2 elv xdomRxRx
4 3 ralbii xdomRxdomRxdomRxRx
5 1 4 mpbi xdomRxRx