Theorem brcnvepres

Description: Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018)

	Ref	Expression
Assertion	brcnvepres	|- ( ( B e. V /\ C e. W ) -> ( B ( `' _E |` A ) C <-> ( B e. A /\ C e. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		brres	|- ( C e. W -> ( B ( `' _E |` A ) C <-> ( B e. A /\ B `' _E C ) ) )
2		brcnvep	|- ( B e. V -> ( B `' _E C <-> C e. B ) )
3	2	anbi2d	|- ( B e. V -> ( ( B e. A /\ B `' _E C ) <-> ( B e. A /\ C e. B ) ) )
4	1 3	sylan9bbr	|- ( ( B e. V /\ C e. W ) -> ( B ( `' _E |` A ) C <-> ( B e. A /\ C e. B ) ) )