Theorem iinconst

Description: Indexed intersection of a constant class, i.e. where B does not depend on x . (Contributed by Mario Carneiro, 6-Feb-2015)

	Ref	Expression
Assertion	iinconst	$$⊢A\ne \varnothing \to \bigcap _{x\in A}B=B$$

Proof

Step	Hyp	Ref	Expression
1		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B\right)$$
2	1	elv	$$⊢y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B$$
3		r19.3rzv	$$⊢A\ne \varnothing \to \left(y\in B\leftrightarrow \forall x\in Ay\in B\right)$$
4	2 3	bitr4id	$$⊢A\ne \varnothing \to \left(y\in \bigcap _{x\in A}B\leftrightarrow y\in B\right)$$
5	4	eqrdv	$$⊢A\ne \varnothing \to \bigcap _{x\in A}B=B$$