Theorem exanres3

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

	Ref	Expression
Assertion	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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elecALTV	|- ( ( u e. _V /\ B e. V ) -> ( B e. [ u ] R <-> u R B ) )
2	1	el2v1	|- ( B e. V -> ( B e. [ u ] R <-> u R B ) )
3		elecALTV	|- ( ( u e. _V /\ C e. W ) -> ( C e. [ u ] S <-> u S C ) )
4	3	el2v1	|- ( C e. W -> ( C e. [ u ] S <-> u S C ) )
5	2 4	bi2anan9	|- ( ( B e. V /\ C e. W ) -> ( ( B e. [ u ] R /\ C e. [ u ] S ) <-> ( u R B /\ u S C ) ) )
6	5	rexbidv	|- ( ( 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 ) ) )