Metamath Proof Explorer

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	\|- ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( A e. [ u ] R /\ B e. [ u ] R ) ) )

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

Step

Hyp

Ref

Expression

 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ R B <-> E. u ( u R A /\ u R B ) ) )

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

1 2

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