Theorem iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

	Ref	Expression
Assertion	iunab	|- U_ x e. A { y | ph } = { y | E. x e. A ph }

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ y A
2		nfab1	|- F/_ y { y | ph }
3	1 2	nfiun	|- F/_ y U_ x e. A { y | ph }
4		nfab1	|- F/_ y { y | E. x e. A ph }
5		abid	|- ( y e. { y | ph } <-> ph )
6	5	rexbii	|- ( E. x e. A y e. { y | ph } <-> E. x e. A ph )
7		eliun	|- ( y e. U_ x e. A { y | ph } <-> E. x e. A y e. { y | ph } )
8		abid	|- ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
9	6 7 8	3bitr4i	|- ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } )
10	3 4 9	eqri	|- U_ x e. A { y | ph } = { y | E. x e. A ph }