Metamath Proof Explorer

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 V R W R I A V


Step Hyp Ref Expression
1 resiexg A V I A V
2 1 adantr A V R W I A V
3 xrnresex A V R W I A V R I A V
4 2 3 mpd3an3 A V R W R I A V