Metamath Proof Explorer


Theorem iunconst

Description: Indexed union of a constant class, i.e. where B does not depend on x . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iunconst A x A B = B

Proof

Step Hyp Ref Expression
1 r19.9rzv A y B x A y B
2 eliun y x A B x A y B
3 1 2 syl6rbbr A y x A B y B
4 3 eqrdv A x A B = B