Metamath Proof Explorer

Theorem br1cossres

Description: B and C are cosets by a restriction: a binary relation. (Contributed by Peter Mazsa, 30-Dec-2018)

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

Step	Hyp	Ref	Expression
1		brcoss	\|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R \|` A ) C <-> E. u ( u ( R \|` A ) B /\ u ( R \|` A ) C ) ) )
2		exanres	\|- ( ( B e. V /\ C e. W ) -> ( E. u ( u ( R \|` A ) B /\ u ( R \|` A ) C ) <-> E. u e. A ( u R B /\ u R C ) ) )
3	1 2	bitrd	\|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R \|` A ) C <-> E. u e. A ( u R B /\ u R C ) ) )

Step

Hyp

Ref

Expression

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

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

1 2

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