Theorem dfiin3

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	dfiun3.1	|- B e. _V
Assertion	dfiin3	|- |^|_ x e. A B = |^| ran ( x e. A |-> B )

Proof

Step	Hyp	Ref	Expression
1		dfiun3.1	|- B e. _V
2		dfiin3g	|- ( A. x e. A B e. _V -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )
3	1	a1i	|- ( x e. A -> B e. _V )
4	2 3	mprg	|- |^|_ x e. A B = |^| ran ( x e. A |-> B )