Theorem dfiin3g

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

	Ref	Expression
Assertion	dfiin3g	|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )

Proof

Step	Hyp	Ref	Expression
1		dfiin2g	|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )
2		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
3	2	rnmpt	|- ran ( x e. A |-> B ) = { y | E. x e. A y = B }
4	3	inteqi	|- |^| ran ( x e. A |-> B ) = |^| { y | E. x e. A y = B }
5	1 4	eqtr4di	|- ( A. x e. A B e. C -> |^|_ x e. A B = |^| ran ( x e. A |-> B ) )