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

Metamath Proof Explorer

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