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

Metamath Proof Explorer

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