Theorem eldmressnsn

Description: The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017)

	Ref	Expression
Assertion	eldmressnsn	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ { 𝐴 } )
2		dmressnsn	⊢ ( 𝐴 ∈ dom 𝐹 → dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } )
3	1 2	eleqtrrd	⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom ( 𝐹 ↾ { 𝐴 } ) )