Theorem elec1cnvres

Description: Elementhood in the converse restricted coset of B . (Contributed by Peter Mazsa, 21-Sep-2018)

	Ref	Expression
Assertion	elec1cnvres	|- ( B e. V -> ( C e. [ B ] `' ( R |` A ) <-> ( C e. A /\ C R B ) ) )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' ( R |` A )
2		relelec	|- ( Rel `' ( R |` A ) -> ( C e. [ B ] `' ( R |` A ) <-> B `' ( R |` A ) C ) )
3	1 2	ax-mp	|- ( C e. [ B ] `' ( R |` A ) <-> B `' ( R |` A ) C )
4		br1cnvres	|- ( B e. V -> ( B `' ( R |` A ) C <-> ( C e. A /\ C R B ) ) )
5	3 4	bitrid	|- ( B e. V -> ( C e. [ B ] `' ( R |` A ) <-> ( C e. A /\ C R B ) ) )