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 } ) } )