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	⊢ ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		eldmressnsn	⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) )
2		elinel2	⊢ ( 𝑋 ∈ ( { 𝑋 } ∩ dom 𝐹 ) → 𝑋 ∈ dom 𝐹 )
3		dmres	⊢ dom ( 𝐹 ↾ { 𝑋 } ) = ( { 𝑋 } ∩ dom 𝐹 )
4	2 3	eleq2s	⊢ ( 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) → 𝑋 ∈ dom 𝐹 )
5	1 4	impbii	⊢ ( 𝑋 ∈ dom 𝐹 ↔ 𝑋 ∈ dom ( 𝐹 ↾ { 𝑋 } ) )