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	3 4	cleqf	|- ( U_ x e. A { y | ph } = { y | E. x e. A ph } <-> A. y ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } ) )
6		abid	|- ( y e. { y | ph } <-> ph )
7	6	rexbii	|- ( E. x e. A y e. { y | ph } <-> E. x e. A ph )
8		eliun	|- ( y e. U_ x e. A { y | ph } <-> E. x e. A y e. { y | ph } )
9		abid	|- ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
10	7 8 9	3bitr4i	|- ( y e. U_ x e. A { y | ph } <-> y e. { y | E. x e. A ph } )
11	5 10	mpgbir	|- U_ x e. A { y | ph } = { y | E. x e. A ph }