Theorem resinsn

Description: Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	resinsn	|- ( ( F |` ( A i^i { B } ) ) = (/) <-> -. B e. ( dom F i^i A ) )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( F |` ( A i^i { B } ) )
2		reldm0	|- ( Rel ( F |` ( A i^i { B } ) ) -> ( ( F |` ( A i^i { B } ) ) = (/) <-> dom ( F |` ( A i^i { B } ) ) = (/) ) )
3	1 2	ax-mp	|- ( ( F |` ( A i^i { B } ) ) = (/) <-> dom ( F |` ( A i^i { B } ) ) = (/) )
4		incom	|- ( ( A i^i { B } ) i^i dom F ) = ( dom F i^i ( A i^i { B } ) )
5		dmres	|- dom ( F |` ( A i^i { B } ) ) = ( ( A i^i { B } ) i^i dom F )
6		inass	|- ( ( dom F i^i A ) i^i { B } ) = ( dom F i^i ( A i^i { B } ) )
7	4 5 6	3eqtr4i	|- dom ( F |` ( A i^i { B } ) ) = ( ( dom F i^i A ) i^i { B } )
8	7	eqeq1i	|- ( dom ( F |` ( A i^i { B } ) ) = (/) <-> ( ( dom F i^i A ) i^i { B } ) = (/) )
9		disjsn	|- ( ( ( dom F i^i A ) i^i { B } ) = (/) <-> -. B e. ( dom F i^i A ) )
10	3 8 9	3bitri	|- ( ( F |` ( A i^i { B } ) ) = (/) <-> -. B e. ( dom F i^i A ) )