Metamath Proof Explorer

Theorem br1cossres2

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

		Ref	Expression
	Assertion	br1cossres2	\|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R \|` A ) C <-> E. x e. A ( B e. [ x ] R /\ C e. [ x ] R ) ) )

Step	Hyp	Ref	Expression
1		br1cossres	\|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R \|` A ) C <-> E. x e. A ( x R B /\ x R C ) ) )
2		exanres3	\|- ( ( B e. V /\ C e. W ) -> ( E. x e. A ( B e. [ x ] R /\ C e. [ x ] R ) <-> E. x e. A ( x R B /\ x R C ) ) )
3	1 2	bitr4d	\|- ( ( B e. V /\ C e. W ) -> ( B ,~ ( R \|` A ) C <-> E. x e. A ( B e. [ x ] R /\ C e. [ x ] R ) ) )

Step

Hyp

Ref

Expression

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

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

1 2

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