Metamath Proof Explorer


Theorem eliuni

Description: Membership in an indexed union, one way. (Contributed by JJ, 27-Jul-2021)

Ref Expression
Hypothesis eliuni.1 x=AB=C
Assertion eliuni ADECExDB

Proof

Step Hyp Ref Expression
1 eliuni.1 x=AB=C
2 1 eleq2d x=AEBEC
3 2 rspcev ADECxDEB
4 eliun ExDBxDEB
5 3 4 sylibr ADECExDB