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

Metamath Proof Explorer

Theorem iinuni

Description: A relationship involving union and indexed intersection. Exercise 23 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iinuni 
|- ( A u. |^| B ) = |^|_ x e. B ( A u. x )

Proof

Step Hyp Ref Expression
1 r19.32v 
 |-  ( A. x e. B ( y e. A \/ y e. x ) <-> ( y e. A \/ A. x e. B y e. x ) )
2 elun 
 |-  ( y e. ( A u. x ) <-> ( y e. A \/ y e. x ) )
3 2 ralbii 
 |-  ( A. x e. B y e. ( A u. x ) <-> A. x e. B ( y e. A \/ y e. x ) )
4 vex 
 |-  y e. _V
5 4 elint2 
 |-  ( y e. |^| B <-> A. x e. B y e. x )
6 5 orbi2i 
 |-  ( ( y e. A \/ y e. |^| B ) <-> ( y e. A \/ A. x e. B y e. x ) )
7 1 3 6 3bitr4ri 
 |-  ( ( y e. A \/ y e. |^| B ) <-> A. x e. B y e. ( A u. x ) )
8 7 abbii 
 |-  { y | ( y e. A \/ y e. |^| B ) } = { y | A. x e. B y e. ( A u. x ) }
9 df-un 
 |-  ( A u. |^| B ) = { y | ( y e. A \/ y e. |^| B ) }
10 df-iin 
 |-  |^|_ x e. B ( A u. x ) = { y | A. x e. B y e. ( A u. x ) }
11 8 9 10 3eqtr4i 
 |-  ( A u. |^| B ) = |^|_ x e. B ( A u. x )