This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( -. <. A , B >. e. ( C X. _V ) -> ( { <. A , B >. } |` C ) = (/) )
8 1 7 nsyl5 
 |-  ( -. A e. C -> ( { <. A , B >. } |` C ) = (/) )