Theorem eliuni

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

	Ref	Expression
Hypothesis	eliuni.1	|- ( x = A -> B = C )
Assertion	eliuni	|- ( ( A e. D /\ E e. C ) -> E e. U_ x e. D B )

Proof

Step	Hyp	Ref	Expression
1		eliuni.1	|- ( x = A -> B = C )
2	1	eleq2d	|- ( x = A -> ( E e. B <-> E e. C ) )
3	2	rspcev	|- ( ( A e. D /\ E e. C ) -> E. x e. D E e. B )
4		eliun	|- ( E e. U_ x e. D B <-> E. x e. D E e. B )
5	3 4	sylibr	|- ( ( A e. D /\ E e. C ) -> E e. U_ x e. D B )