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 A B = B

Proof

Step Hyp Ref Expression
1 r19.3rzv A y B x A y B
2 eliin y V y x A B x A y B
3 2 elv y x A B x A y B
4 1 3 syl6rbbr A y x A B y B
5 4 eqrdv A x A B = B