Metamath Proof Explorer


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 r19.3rzv
 |-  ( A =/= (/) -> ( y e. B <-> A. x e. A y e. B ) )
2 eliin
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
3 2 elv
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
4 1 3 syl6rbbr
 |-  ( A =/= (/) -> ( y e. |^|_ x e. A B <-> y e. B ) )
5 4 eqrdv
 |-  ( A =/= (/) -> |^|_ x e. A B = B )