Theorem dfuni2

Description: Alternate definition of class union. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	dfuni2	|- U. A = { x | E. y e. A x e. y }

Proof

Step	Hyp	Ref	Expression
1		df-uni	|- U. A = { x | E. y ( x e. y /\ y e. A ) }
2		exancom	|- ( E. y ( x e. y /\ y e. A ) <-> E. y ( y e. A /\ x e. y ) )
3		df-rex	|- ( E. y e. A x e. y <-> E. y ( y e. A /\ x e. y ) )
4	2 3	bitr4i	|- ( E. y ( x e. y /\ y e. A ) <-> E. y e. A x e. y )
5	4	abbii	|- { x | E. y ( x e. y /\ y e. A ) } = { x | E. y e. A x e. y }
6	1 5	eqtri	|- U. A = { x | E. y e. A x e. y }