Theorem uniel

Description: Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025)

	Ref	Expression
Assertion	uniel	$$⊢\bigcup A\in B\leftrightarrow \exists x\in B\forall z\left(z\in x\leftrightarrow \exists y\in Az\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		clabel	$$⊢\left\{z|\exists y\in Az\in y\right\}\in B\leftrightarrow \exists x\left(x\in B\wedge \forall z\left(z\in x\leftrightarrow \exists y\in Az\in y\right)\right)$$
2		dfuni2	$$⊢\bigcup A=\left\{z|\exists y\in Az\in y\right\}$$
3	2	eleq1i	$$⊢\bigcup A\in B\leftrightarrow \left\{z|\exists y\in Az\in y\right\}\in B$$
4		df-rex	$$⊢\exists x\in B\forall z\left(z\in x\leftrightarrow \exists y\in Az\in y\right)\leftrightarrow \exists x\left(x\in B\wedge \forall z\left(z\in x\leftrightarrow \exists y\in Az\in y\right)\right)$$
5	1 3 4	3bitr4i	$$⊢\bigcup A\in B\leftrightarrow \exists x\in B\forall z\left(z\in x\leftrightarrow \exists y\in Az\in y\right)$$