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