Theorem iinconst

Description: Indexed intersection of a constant class, i.e. where B does not depend on x . (Contributed by Mario Carneiro, 6-Feb-2015)

	Ref	Expression
Assertion	iinconst	|- ( A =/= (/) -> |^|_ x e. A B = B )

Proof

Step	Hyp	Ref	Expression
1		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
2	1	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
3		r19.3rzv	|- ( A =/= (/) -> ( y e. B <-> A. x e. A y e. B ) )
4	2 3	bitr4id	|- ( A =/= (/) -> ( y e. |^|_ x e. A B <-> y e. B ) )
5	4	eqrdv	|- ( A =/= (/) -> |^|_ x e. A B = B )