Theorem exan3

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

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

Proof

Step	Hyp	Ref	Expression
1		elecALTV	|- ( ( u e. _V /\ A e. V ) -> ( A e. [ u ] R <-> u R A ) )
2	1	el2v1	|- ( A e. V -> ( A e. [ u ] R <-> u R A ) )
3		elecALTV	|- ( ( u e. _V /\ B e. W ) -> ( B e. [ u ] R <-> u R B ) )
4	3	el2v1	|- ( B e. W -> ( B e. [ u ] R <-> u R B ) )
5	2 4	bi2anan9	|- ( ( A e. V /\ B e. W ) -> ( ( A e. [ u ] R /\ B e. [ u ] R ) <-> ( u R A /\ u R B ) ) )
6	5	exbidv	|- ( ( A e. V /\ B e. W ) -> ( E. u ( A e. [ u ] R /\ B e. [ u ] R ) <-> E. u ( u R A /\ u R B ) ) )