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

Metamath Proof Explorer

Theorem mptsuppdifd

Description: The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019)

Ref Expression
Hypotheses mptsuppdifd.f 
|- F = ( x e. A |-> B )
mptsuppdifd.a 
|- ( ph -> A e. V )
mptsuppdifd.z 
|- ( ph -> Z e. W )
Assertion mptsuppdifd 
|- ( ph -> ( F supp Z ) = { x e. A | B e. ( _V \ { Z } ) } )

Proof

Step Hyp Ref Expression
1 mptsuppdifd.f 
 |-  F = ( x e. A |-> B )
2 mptsuppdifd.a 
 |-  ( ph -> A e. V )
3 mptsuppdifd.z 
 |-  ( ph -> Z e. W )
4 2 mptexd 
 |-  ( ph -> ( x e. A |-> B ) e. _V )
5 1 4 eqeltrid 
 |-  ( ph -> F e. _V )
6 suppimacnv 
 |-  ( ( F e. _V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
7 5 3 6 syl2anc 
 |-  ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
8 1 mptpreima 
 |-  ( `' F " ( _V \ { Z } ) ) = { x e. A | B e. ( _V \ { Z } ) }
9 7 8 eqtrdi 
 |-  ( ph -> ( F supp Z ) = { x e. A | B e. ( _V \ { Z } ) } )