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 )