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	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
2		uniexg	⊢ ( ∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V )
3		ssun2	⊢ ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
4		dmrnssfld	⊢ ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴
5	3 4	sstri	⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg	⊢ ( ( ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V ) → ran 𝐴 ∈ V )
7	5 6	mpan	⊢ ( ∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V )
8	1 2 7	3syl	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )