Theorem brcoels

Description: B and C are coelements : a binary relation. (Contributed by Peter Mazsa, 14-Jan-2020) (Revised by Peter Mazsa, 5-Oct-2021)

	Ref	Expression
Assertion	brcoels	|- ( ( B e. V /\ C e. W ) -> ( B ~ A C <-> E. u e. A ( B e. u /\ C e. u ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( x = B -> ( x e. u <-> B e. u ) )
2		eleq1	|- ( y = C -> ( y e. u <-> C e. u ) )
3	1 2	bi2anan9	|- ( ( x = B /\ y = C ) -> ( ( x e. u /\ y e. u ) <-> ( B e. u /\ C e. u ) ) )
4	3	rexbidv	|- ( ( x = B /\ y = C ) -> ( E. u e. A ( x e. u /\ y e. u ) <-> E. u e. A ( B e. u /\ C e. u ) ) )
5		dfcoels	|- ~ A = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
6	4 5	brabga	|- ( ( B e. V /\ C e. W ) -> ( B ~ A C <-> E. u e. A ( B e. u /\ C e. u ) ) )