Theorem suppimacnvss

Description: The support of functions "defined" by inverse images is a subset of the support defined by df-supp . (Contributed by AV, 7-Apr-2019)

	Ref	Expression
Assertion	suppimacnvss	|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) C_ ( R supp Z ) )

Proof

Step	Hyp	Ref	Expression
1		exsimpl	|- ( E. y ( x R y /\ y =/= Z ) -> E. y x R y )
2		pm5.1	|- ( ( x R y /\ y =/= Z ) -> ( x R y <-> y =/= Z ) )
3	2	eximi	|- ( E. y ( x R y /\ y =/= Z ) -> E. y ( x R y <-> y =/= Z ) )
4	1 3	jca	|- ( E. y ( x R y /\ y =/= Z ) -> ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) )
5	4	a1i	|- ( ( R e. V /\ Z e. W ) -> ( E. y ( x R y /\ y =/= Z ) -> ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) ) )
6	5	ss2abdv	|- ( ( R e. V /\ Z e. W ) -> { x | E. y ( x R y /\ y =/= Z ) } C_ { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )
7		cnvimadfsn	|- ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) }
8	7	a1i	|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) } )
9		suppvalbr	|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )
10	6 8 9	3sstr4d	|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) C_ ( R supp Z ) )