Theorem dfiin2

Description: Alternate definition of indexed intersection when B is a set. Definition 15(b) of Suppes p. 44. (Contributed by NM, 28-Jun-1998) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Hypothesis	dfiun2.1	|- B e. _V
Assertion	dfiin2	|- |^|_ x e. A B = |^| { y | E. x e. A y = B }

Proof

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