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	|- ( B e. dom ( F |` { A } ) -> B = A )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( B e. ( { A } i^i dom F ) <-> ( B e. { A } /\ B e. dom F ) )
2		elsni	|- ( B e. { A } -> B = A )
3	2	adantr	|- ( ( B e. { A } /\ B e. dom F ) -> B = A )
4	1 3	sylbi	|- ( B e. ( { A } i^i dom F ) -> B = A )
5		dmres	|- dom ( F |` { A } ) = ( { A } i^i dom F )
6	4 5	eleq2s	|- ( B e. dom ( F |` { A } ) -> B = A )