This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in dom F \leftrightarrow X \in dom ({F ↾}_{\{X\}})$

Proof

Step	Hyp	Ref	Expression
1		eldmressnsn	$⊢ X \in dom F \to X \in dom ({F ↾}_{\{X\}})$
2		elinel2	$⊢ X \in (\{X\} \cap dom F) \to X \in dom F$
3		dmres	$⊢ dom ({F ↾}_{\{X\}}) = \{X\} \cap dom F$
4	2 3	eleq2s	$⊢ X \in dom ({F ↾}_{\{X\}}) \to X \in dom F$
5	1 4	impbii	$⊢ X \in dom F \leftrightarrow X \in dom ({F ↾}_{\{X\}})$