Theorem iinexd

Description: The existence of an indexed union. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	iinexd.1	$$⊢\phi \to A\ne \varnothing$$
	iinexd.2	$$⊢\phi \to \forall x\in AB\in C$$
Assertion	iinexd	$$⊢\phi \to \bigcap _{x\in A}B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iinexd.1	$$⊢\phi \to A\ne \varnothing$$
2		iinexd.2	$$⊢\phi \to \forall x\in AB\in C$$
3		iinexg	$$⊢\left(A\ne \varnothing \wedge \forall x\in AB\in C\right)\to \bigcap _{x\in A}B\in \mathrm{V}$$
4	1 2 3	syl2anc	$$⊢\phi \to \bigcap _{x\in A}B\in \mathrm{V}$$