Metamath Proof Explorer

Theorem exanres

Description: Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021)

Ref Expression
Assertion exanres 
|- ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> E. u e. A ( u R B /\ u S C ) ) )

Proof

Step Hyp Ref Expression
1 brres 
 |-  ( B e. V -> ( u ( R |` A ) B <-> ( u e. A /\ u R B ) ) )
2 brres 
 |-  ( C e. W -> ( u ( S |` A ) C <-> ( u e. A /\ u S C ) ) )
3 1 2 bi2anan9 
 |-  ( ( B e. V /\ C e. W ) -> ( ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> ( ( u e. A /\ u R B ) /\ ( u e. A /\ u S C ) ) ) )
4 anandi 
 |-  ( ( u e. A /\ ( u R B /\ u S C ) ) <-> ( ( u e. A /\ u R B ) /\ ( u e. A /\ u S C ) ) )
5 3 4 bitr4di 
 |-  ( ( B e. V /\ C e. W ) -> ( ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> ( u e. A /\ ( u R B /\ u S C ) ) ) )
6 5 exbidv 
 |-  ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> E. u ( u e. A /\ ( u R B /\ u S C ) ) ) )
7 df-rex 
 |-  ( E. u e. A ( u R B /\ u S C ) <-> E. u ( u e. A /\ ( u R B /\ u S C ) ) )
8 6 7 bitr4di 
 |-  ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> E. u e. A ( u R B /\ u S C ) ) )