Theorem xrncnvepresex

Description: Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020) (Revised by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	xrncnvepresex	|- ( ( A e. V /\ R e. W ) -> ( R |X. ( `' _E |` A ) ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	|- ( A e. V -> ( `' _E |` A ) e. _V )
2	1	adantr	|- ( ( A e. V /\ R e. W ) -> ( `' _E |` A ) e. _V )
3		xrnresex	|- ( ( A e. V /\ R e. W /\ ( `' _E |` A ) e. _V ) -> ( R |X. ( `' _E |` A ) ) e. _V )
4	2 3	mpd3an3	|- ( ( A e. V /\ R e. W ) -> ( R |X. ( `' _E |` A ) ) e. _V )