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
|- A. x e. dom ,~ R x ,~ R x

Proof

Step Hyp Ref Expression
1 ralel
 |-  A. x e. dom ,~ R x e. dom ,~ R
2 eldmcoss2
 |-  ( x e. _V -> ( x e. dom ,~ R <-> x ,~ R x ) )
3 2 elv
 |-  ( x e. dom ,~ R <-> x ,~ R x )
4 3 ralbii
 |-  ( A. x e. dom ,~ R x e. dom ,~ R <-> A. x e. dom ,~ R x ,~ R x )
5 1 4 mpbi
 |-  A. x e. dom ,~ R x ,~ R x