Metamath Proof Explorer

Theorem exanres2

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

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

Step	Hyp	Ref	Expression
1		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 ) ) )
2		exanres3	\|- ( ( B e. V /\ C e. W ) -> ( E. u e. A ( B e. [ u ] R /\ C e. [ u ] S ) <-> E. u e. A ( u R B /\ u S C ) ) )
3	1 2	bitr4d	\|- ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R \|` A ) B /\ u ( S \|` A ) C ) <-> E. u e. A ( B e. [ u ] R /\ C e. [ u ] S ) ) )

Step

Hyp

Ref

Expression

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

 |-  ( ( B e. V /\ C e. W ) -> ( E. u e. A ( B e. [ u ] R /\ C e. [ u ] S ) <-> E. u e. A ( u R B /\ u S C ) ) )

1 2

 |-  ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R |` A ) B /\ u ( S |` A ) C ) <-> E. u e. A ( B e. [ u ] R /\ C e. [ u ] S ) ) )