Theorem ressnop0

Description: If A is not in C , then the restriction of a singleton of <. A , B >. to C is null. (Contributed by Scott Fenton, 15-Apr-2011)

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

Proof

Step	Hyp	Ref	Expression
1		opelxp1	|- ( <. A , B >. e. ( C X. _V ) -> A e. C )
2		df-res	|- ( { <. A , B >. } |` C ) = ( { <. A , B >. } i^i ( C X. _V ) )
3		incom	|- ( { <. A , B >. } i^i ( C X. _V ) ) = ( ( C X. _V ) i^i { <. A , B >. } )
4	2 3	eqtri	|- ( { <. A , B >. } |` C ) = ( ( C X. _V ) i^i { <. A , B >. } )
5		disjsn	|- ( ( ( C X. _V ) i^i { <. A , B >. } ) = (/) <-> -. <. A , B >. e. ( C X. _V ) )
6	5	biimpri	|- ( -. <. A , B >. e. ( C X. _V ) -> ( ( C X. _V ) i^i { <. A , B >. } ) = (/) )
7	4 6	syl5eq	|- ( -. <. A , B >. e. ( C X. _V ) -> ( { <. A , B >. } |` C ) = (/) )
8	1 7	nsyl5	|- ( -. A e. C -> ( { <. A , B >. } |` C ) = (/) )