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	|- ( U. A e. B <-> E. x e. B A. z ( z e. x <-> E. y e. A z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		clabel	|- ( { z | E. y e. A z e. y } e. B <-> E. x ( x e. B /\ A. z ( z e. x <-> E. y e. A z e. y ) ) )
2		dfuni2	|- U. A = { z | E. y e. A z e. y }
3	2	eleq1i	|- ( U. A e. B <-> { z | E. y e. A z e. y } e. B )
4		df-rex	|- ( E. x e. B A. z ( z e. x <-> E. y e. A z e. y ) <-> E. x ( x e. B /\ A. z ( z e. x <-> E. y e. A z e. y ) ) )
5	1 3 4	3bitr4i	|- ( U. A e. B <-> E. x e. B A. z ( z e. x <-> E. y e. A z e. y ) )