Theorem eccnvepres

Description: Restricted converse epsilon coset of B . (Contributed by Peter Mazsa, 11-Feb-2018) (Revised by Peter Mazsa, 21-Oct-2021)

	Ref	Expression
Assertion	eccnvepres	|- ( B e. V -> [ B ] ( `' _E |` A ) = { x e. B | B e. A } )

Proof

Step	Hyp	Ref	Expression
1		brcnvep	|- ( B e. V -> ( B `' _E x <-> x e. B ) )
2	1	anbi1cd	|- ( B e. V -> ( ( B e. A /\ B `' _E x ) <-> ( x e. B /\ B e. A ) ) )
3	2	abbidv	|- ( B e. V -> { x | ( B e. A /\ B `' _E x ) } = { x | ( x e. B /\ B e. A ) } )
4		ecres	|- [ B ] ( `' _E |` A ) = { x | ( B e. A /\ B `' _E x ) }
5		df-rab	|- { x e. B | B e. A } = { x | ( x e. B /\ B e. A ) }
6	3 4 5	3eqtr4g	|- ( B e. V -> [ B ] ( `' _E |` A ) = { x e. B | B e. A } )