Theorem xrnidresex

Description: Sufficient condition for a range Cartesian product with restricted identity to be a set. (Contributed by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	xrnidresex	|- ( ( A e. V /\ R e. W ) -> ( R |X. ( _I |` A ) ) e. _V )

Proof

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