Theorem dmexg

Description: The domain of a set is a set. Corollary 6.8(2) of TakeutiZaring p. 26. (Contributed by NM, 7-Apr-1995)

	Ref	Expression
Assertion	dmexg	⊢ ( 𝐴 ∈ 𝑉 → dom 𝐴 ∈ V )

Proof

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