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

Metamath Proof Explorer

Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fnresdisj 
|- ( F Fn A -> ( ( A i^i B ) = (/) <-> ( F |` B ) = (/) ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( F |` B )
2 reldm0 
 |-  ( Rel ( F |` B ) -> ( ( F |` B ) = (/) <-> dom ( F |` B ) = (/) ) )
3 1 2 ax-mp 
 |-  ( ( F |` B ) = (/) <-> dom ( F |` B ) = (/) )
4 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
5 incom 
 |-  ( B i^i dom F ) = ( dom F i^i B )
6 4 5 eqtri 
 |-  dom ( F |` B ) = ( dom F i^i B )
7 fndm 
 |-  ( F Fn A -> dom F = A )
8 7 ineq1d 
 |-  ( F Fn A -> ( dom F i^i B ) = ( A i^i B ) )
9 6 8 eqtrid 
 |-  ( F Fn A -> dom ( F |` B ) = ( A i^i B ) )
10 9 eqeq1d 
 |-  ( F Fn A -> ( dom ( F |` B ) = (/) <-> ( A i^i B ) = (/) ) )
11 3 10 bitr2id 
 |-  ( F Fn A -> ( ( A i^i B ) = (/) <-> ( F |` B ) = (/) ) )