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

Metamath Proof Explorer

Theorem iunin1f

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use uniiun to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004) (Revised by Thierry Arnoux, 2-May-2020)

Ref Expression
Hypothesis iunin1f.1 
|- F/_ x C
Assertion iunin1f 
|- U_ x e. A ( B i^i C ) = ( U_ x e. A B i^i C )

Proof

Step Hyp Ref Expression
1 iunin1f.1 
 |-  F/_ x C
2 1 nfcri 
 |-  F/ x y e. C
3 2 r19.41 
 |-  ( E. x e. A ( y e. B /\ y e. C ) <-> ( E. x e. A y e. B /\ y e. C ) )
4 elin 
 |-  ( y e. ( B i^i C ) <-> ( y e. B /\ y e. C ) )
5 4 rexbii 
 |-  ( E. x e. A y e. ( B i^i C ) <-> E. x e. A ( y e. B /\ y e. C ) )
6 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
7 6 anbi1i 
 |-  ( ( y e. U_ x e. A B /\ y e. C ) <-> ( E. x e. A y e. B /\ y e. C ) )
8 3 5 7 3bitr4i 
 |-  ( E. x e. A y e. ( B i^i C ) <-> ( y e. U_ x e. A B /\ y e. C ) )
9 eliun 
 |-  ( y e. U_ x e. A ( B i^i C ) <-> E. x e. A y e. ( B i^i C ) )
10 elin 
 |-  ( y e. ( U_ x e. A B i^i C ) <-> ( y e. U_ x e. A B /\ y e. C ) )
11 8 9 10 3bitr4i 
 |-  ( y e. U_ x e. A ( B i^i C ) <-> y e. ( U_ x e. A B i^i C ) )
12 11 eqriv 
 |-  U_ x e. A ( B i^i C ) = ( U_ x e. A B i^i C )