This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ V → dom ⁡ A ∈ V

Proof

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