Metamath Proof Explorer

Theorem rexsupp

Description: Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by AV, 27-May-2019)

Ref Expression
Assertion rexsupp 
|- ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( E. x e. ( F supp Z ) ph <-> E. x e. X ( ( F ` x ) =/= Z /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 elsuppfn 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( x e. ( F supp Z ) <-> ( x e. X /\ ( F ` x ) =/= Z ) ) )
2 1 anbi1d 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( ( x e. ( F supp Z ) /\ ph ) <-> ( ( x e. X /\ ( F ` x ) =/= Z ) /\ ph ) ) )
3 anass 
 |-  ( ( ( x e. X /\ ( F ` x ) =/= Z ) /\ ph ) <-> ( x e. X /\ ( ( F ` x ) =/= Z /\ ph ) ) )
4 2 3 bitrdi 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( ( x e. ( F supp Z ) /\ ph ) <-> ( x e. X /\ ( ( F ` x ) =/= Z /\ ph ) ) ) )
5 4 rexbidv2 
 |-  ( ( F Fn X /\ X e. V /\ Z e. W ) -> ( E. x e. ( F supp Z ) ph <-> E. x e. X ( ( F ` x ) =/= Z /\ ph ) ) )