Theorem snres0

Description: Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypothesis	snres0.1	|- B e. _V
Assertion	snres0	|- ( ( { <. A , B >. } |` C ) = (/) <-> -. A e. C )

Proof

Step	Hyp	Ref	Expression
1		snres0.1	|- B e. _V
2		relres	|- Rel ( { <. A , B >. } |` C )
3		reldm0	|- ( Rel ( { <. A , B >. } |` C ) -> ( ( { <. A , B >. } |` C ) = (/) <-> dom ( { <. A , B >. } |` C ) = (/) ) )
4	2 3	ax-mp	|- ( ( { <. A , B >. } |` C ) = (/) <-> dom ( { <. A , B >. } |` C ) = (/) )
5		dmres	|- dom ( { <. A , B >. } |` C ) = ( C i^i dom { <. A , B >. } )
6	1	dmsnop	|- dom { <. A , B >. } = { A }
7	6	ineq2i	|- ( C i^i dom { <. A , B >. } ) = ( C i^i { A } )
8	5 7	eqtri	|- dom ( { <. A , B >. } |` C ) = ( C i^i { A } )
9	8	eqeq1i	|- ( dom ( { <. A , B >. } |` C ) = (/) <-> ( C i^i { A } ) = (/) )
10		disjsn	|- ( ( C i^i { A } ) = (/) <-> -. A e. C )
11	4 9 10	3bitri	|- ( ( { <. A , B >. } |` C ) = (/) <-> -. A e. C )