Theorem dfiun2

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 27-Jun-1998) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypothesis	dfiun2.1	|- B e. _V
Assertion	dfiun2	|- U_ x e. A B = U. { y | E. x e. A y = B }

Proof

Step	Hyp	Ref	Expression
1		dfiun2.1	|- B e. _V
2		dfiun2g	|- ( A. x e. A B e. _V -> U_ x e. A B = U. { y | E. x e. A y = B } )
3	1	a1i	|- ( x e. A -> B e. _V )
4	2 3	mprg	|- U_ x e. A B = U. { y | E. x e. A y = B }