Metamath Proof Explorer

Theorem eliunid

Description: Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Assertion eliunid 
|- ( ( x e. A /\ C e. B ) -> C e. U_ x e. A B )

Proof

Step Hyp Ref Expression
1 rspe 
 |-  ( ( x e. A /\ C e. B ) -> E. x e. A C e. B )
2 eliun 
 |-  ( C e. U_ x e. A B <-> E. x e. A C e. B )
3 1 2 sylibr 
 |-  ( ( x e. A /\ C e. B ) -> C e. U_ x e. A B )