Metamath Proof Explorer

Theorem dmuni

Description: The domain of a union. Part of Exercise 8 of Enderton p. 41. (Contributed by NM, 3-Feb-2004)

Ref Expression
Assertion dmuni 
|- dom U. A = U_ x e. A dom x

Proof

Step Hyp Ref Expression
1 excom 
 |-  ( E. z E. x ( <. y , z >. e. x /\ x e. A ) <-> E. x E. z ( <. y , z >. e. x /\ x e. A ) )
2 ancom 
 |-  ( ( E. z <. y , z >. e. x /\ x e. A ) <-> ( x e. A /\ E. z <. y , z >. e. x ) )
3 19.41v 
 |-  ( E. z ( <. y , z >. e. x /\ x e. A ) <-> ( E. z <. y , z >. e. x /\ x e. A ) )
4 vex 
 |-  y e. _V
5 4 eldm2 
 |-  ( y e. dom x <-> E. z <. y , z >. e. x )
6 5 anbi2i 
 |-  ( ( x e. A /\ y e. dom x ) <-> ( x e. A /\ E. z <. y , z >. e. x ) )
7 2 3 6 3bitr4i 
 |-  ( E. z ( <. y , z >. e. x /\ x e. A ) <-> ( x e. A /\ y e. dom x ) )
8 7 exbii 
 |-  ( E. x E. z ( <. y , z >. e. x /\ x e. A ) <-> E. x ( x e. A /\ y e. dom x ) )
9 1 8 bitri 
 |-  ( E. z E. x ( <. y , z >. e. x /\ x e. A ) <-> E. x ( x e. A /\ y e. dom x ) )
10 eluni 
 |-  ( <. y , z >. e. U. A <-> E. x ( <. y , z >. e. x /\ x e. A ) )
11 10 exbii 
 |-  ( E. z <. y , z >. e. U. A <-> E. z E. x ( <. y , z >. e. x /\ x e. A ) )
12 df-rex 
 |-  ( E. x e. A y e. dom x <-> E. x ( x e. A /\ y e. dom x ) )
13 9 11 12 3bitr4i 
 |-  ( E. z <. y , z >. e. U. A <-> E. x e. A y e. dom x )
14 4 eldm2 
 |-  ( y e. dom U. A <-> E. z <. y , z >. e. U. A )
15 eliun 
 |-  ( y e. U_ x e. A dom x <-> E. x e. A y e. dom x )
16 13 14 15 3bitr4i 
 |-  ( y e. dom U. A <-> y e. U_ x e. A dom x )
17 16 eqriv 
 |-  dom U. A = U_ x e. A dom x