Theorem gruiin

Description: A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruiin	|- ( ( U e. Univ /\ E. x e. A B e. U ) -> |^|_ x e. A B e. U )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ x U e. Univ
2		nfii1	|- F/_ x |^|_ x e. A B
3	2	nfel1	|- F/ x |^|_ x e. A B e. U
4		iinss2	|- ( x e. A -> |^|_ x e. A B C_ B )
5		gruss	|- ( ( U e. Univ /\ B e. U /\ |^|_ x e. A B C_ B ) -> |^|_ x e. A B e. U )
6	4 5	syl3an3	|- ( ( U e. Univ /\ B e. U /\ x e. A ) -> |^|_ x e. A B e. U )
7	6	3exp	|- ( U e. Univ -> ( B e. U -> ( x e. A -> |^|_ x e. A B e. U ) ) )
8	7	com23	|- ( U e. Univ -> ( x e. A -> ( B e. U -> |^|_ x e. A B e. U ) ) )
9	1 3 8	rexlimd	|- ( U e. Univ -> ( E. x e. A B e. U -> |^|_ x e. A B e. U ) )
10	9	imp	|- ( ( U e. Univ /\ E. x e. A B e. U ) -> |^|_ x e. A B e. U )