Metamath Proof Explorer

Theorem brcosscnv2

Description: A and B are cosets by converse R : a binary relation. (Contributed by Peter Mazsa, 12-Mar-2019)

		Ref	Expression
	Assertion	brcosscnv2	\|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> ( [ A ] R i^i [ B ] R ) =/= (/) ) )

Step	Hyp	Ref	Expression
1		brcosscnv	\|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> E. x ( A R x /\ B R x ) ) )
2		ecinn0	\|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> E. x ( A R x /\ B R x ) ) )
3	1 2	bitr4d	\|- ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> ( [ A ] R i^i [ B ] R ) =/= (/) ) )

Step

Hyp

Ref

Expression

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

 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> E. x ( A R x /\ B R x ) ) )

1 2

 |-  ( ( A e. V /\ B e. W ) -> ( A ,~ `' R B <-> ( [ A ] R i^i [ B ] R ) =/= (/) ) )