Theorem brcoss2

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

	Ref	Expression
Assertion	brcoss2	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr RB\leftrightarrow \exists u\left(A\in \left[u\right]R\wedge B\in \left[u\right]R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brcoss	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr RB\leftrightarrow \exists u\left(uRA\wedge uRB\right)\right)$$
2		exan3	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\exists u\left(A\in \left[u\right]R\wedge B\in \left[u\right]R\right)\leftrightarrow \exists u\left(uRA\wedge uRB\right)\right)$$
3	1 2	bitr4d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\wr RB\leftrightarrow \exists u\left(A\in \left[u\right]R\wedge B\in \left[u\right]R\right)\right)$$