Theorem eldmeldmressn

Description: An element of the domain (of a relation) is an element of the domain of the restriction (of the relation) to the singleton containing this element. (Contributed by Alexander van der Vekens, 22-Jul-2018)

	Ref	Expression
Assertion	eldmeldmressn	|- ( X e. dom F <-> X e. dom ( F |` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		eldmressnsn	|- ( X e. dom F -> X e. dom ( F |` { X } ) )
2		elinel2	|- ( X e. ( { X } i^i dom F ) -> X e. dom F )
3		dmres	|- dom ( F |` { X } ) = ( { X } i^i dom F )
4	2 3	eleq2s	|- ( X e. dom ( F |` { X } ) -> X e. dom F )
5	1 4	impbii	|- ( X e. dom F <-> X e. dom ( F |` { X } ) )