Theorem eldmressn

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

	Ref	Expression
Assertion	eldmressn	⊢ ( 𝐵 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → 𝐵 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝐵 ∈ ( { 𝐴 } ∩ dom 𝐹 ) ↔ ( 𝐵 ∈ { 𝐴 } ∧ 𝐵 ∈ dom 𝐹 ) )
2		elsni	⊢ ( 𝐵 ∈ { 𝐴 } → 𝐵 = 𝐴 )
3	2	adantr	⊢ ( ( 𝐵 ∈ { 𝐴 } ∧ 𝐵 ∈ dom 𝐹 ) → 𝐵 = 𝐴 )
4	1 3	sylbi	⊢ ( 𝐵 ∈ ( { 𝐴 } ∩ dom 𝐹 ) → 𝐵 = 𝐴 )
5		dmres	⊢ dom ( 𝐹 ↾ { 𝐴 } ) = ( { 𝐴 } ∩ dom 𝐹 )
6	4 5	eleq2s	⊢ ( 𝐵 ∈ dom ( 𝐹 ↾ { 𝐴 } ) → 𝐵 = 𝐴 )