Theorem resinsn

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

	Ref	Expression
Assertion	resinsn	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) )
2		reldm0	⊢ ( Rel ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ) )
3	1 2	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ )
4		incom	⊢ ( ( 𝐴 ∩ { 𝐵 } ) ∩ dom 𝐹 ) = ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) )
5		dmres	⊢ dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ( ( 𝐴 ∩ { 𝐵 } ) ∩ dom 𝐹 )
6		inass	⊢ ( ( dom 𝐹 ∩ 𝐴 ) ∩ { 𝐵 } ) = ( dom 𝐹 ∩ ( 𝐴 ∩ { 𝐵 } ) )
7	4 5 6	3eqtr4i	⊢ dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ( ( dom 𝐹 ∩ 𝐴 ) ∩ { 𝐵 } )
8	7	eqeq1i	⊢ ( dom ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ( ( dom 𝐹 ∩ 𝐴 ) ∩ { 𝐵 } ) = ∅ )
9		disjsn	⊢ ( ( ( dom 𝐹 ∩ 𝐴 ) ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )
10	3 8 9	3bitri	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ { 𝐵 } ) ) = ∅ ↔ ¬ 𝐵 ∈ ( dom 𝐹 ∩ 𝐴 ) )