Theorem mptsuppd

Description: The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019) (Revised 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 )
	mptsuppd.b	|- ( ( ph /\ x e. A ) -> B e. U )
Assertion	mptsuppd	|- ( ph -> ( F supp Z ) = { x e. A | B =/= 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		mptsuppd.b	|- ( ( ph /\ x e. A ) -> B e. U )
5	1 2 3	mptsuppdifd	|- ( ph -> ( F supp Z ) = { x e. A | B e. ( _V \ { Z } ) } )
6		eldifsn	|- ( B e. ( _V \ { Z } ) <-> ( B e. _V /\ B =/= Z ) )
7	4	elexd	|- ( ( ph /\ x e. A ) -> B e. _V )
8	7	biantrurd	|- ( ( ph /\ x e. A ) -> ( B =/= Z <-> ( B e. _V /\ B =/= Z ) ) )
9	6 8	bitr4id	|- ( ( ph /\ x e. A ) -> ( B e. ( _V \ { Z } ) <-> B =/= Z ) )
10	9	rabbidva	|- ( ph -> { x e. A | B e. ( _V \ { Z } ) } = { x e. A | B =/= Z } )
11	5 10	eqtrd	|- ( ph -> ( F supp Z ) = { x e. A | B =/= Z } )