Theorem iunconst

Description: Indexed union of a constant class, i.e. where B does not depend on x . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		eliun	$$⊢y\in \bigcup _{x\in A}B\leftrightarrow \exists x\in Ay\in B$$
2		r19.9rzv	$$⊢A\ne \varnothing \to \left(y\in B\leftrightarrow \exists x\in Ay\in B\right)$$
3	1 2	bitr4id	$$⊢A\ne \varnothing \to \left(y\in \bigcup _{x\in A}B\leftrightarrow y\in B\right)$$
4	3	eqrdv	$$⊢A\ne \varnothing \to \bigcup _{x\in A}B=B$$