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 =/= (/) -> U_ x e. A B = B )

Proof

Step Hyp Ref Expression
1 r19.9rzv
 |-  ( A =/= (/) -> ( y e. B <-> E. x e. A y e. B ) )
2 eliun
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
3 1 2 syl6rbbr
 |-  ( A =/= (/) -> ( y e. U_ x e. A B <-> y e. B ) )
4 3 eqrdv
 |-  ( A =/= (/) -> U_ x e. A B = B )