Metamath Proof Explorer

Theorem suppssdm

Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019)

Ref Expression
Assertion suppssdm 
|- ( F supp Z ) C_ dom F

Proof

Step Hyp Ref Expression
1 suppval 
 |-  ( ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = { i e. dom F | ( F " { i } ) =/= { Z } } )
2 ssrab2 
 |-  { i e. dom F | ( F " { i } ) =/= { Z } } C_ dom F
3 1 2 eqsstrdi 
 |-  ( ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ dom F )
4 supp0prc 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
5 0ss 
 |-  (/) C_ dom F
6 4 5 eqsstrdi 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ dom F )
7 3 6 pm2.61i 
 |-  ( F supp Z ) C_ dom F