Metamath Proof Explorer

Theorem ress0

Description: All restrictions of the null set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion ress0 
|- ( (/) |`s A ) = (/)

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ A
2 0ex 
 |-  (/) e. _V
3 eqid 
 |-  ( (/) |`s A ) = ( (/) |`s A )
4 base0 
 |-  (/) = ( Base ` (/) )
5 3 4 ressid2 
 |-  ( ( (/) C_ A /\ (/) e. _V /\ A e. _V ) -> ( (/) |`s A ) = (/) )
6 1 2 5 mp3an12 
 |-  ( A e. _V -> ( (/) |`s A ) = (/) )
7 reldmress 
 |-  Rel dom |`s
8 7 ovprc2 
 |-  ( -. A e. _V -> ( (/) |`s A ) = (/) )
9 6 8 pm2.61i 
 |-  ( (/) |`s A ) = (/)