Metamath Proof Explorer

Theorem rnexg

Description: The range of a set is a set. Corollary 6.8(3) of TakeutiZaring p. 26. Similar to Lemma 3D of Enderton p. 41. (Contributed by NM, 31-Mar-1995)

Ref Expression
Assertion rnexg A V ran A V


Step Hyp Ref Expression
1 uniexg A V A V
2 uniexg A V A V
3 ssun2 ran A dom A ran A
4 dmrnssfld dom A ran A A
5 3 4 sstri ran A A
6 ssexg ran A A A V ran A V
7 5 6 mpan A V ran A V
8 1 2 7 3syl A V ran A V