Theorem eliuni

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

	Ref	Expression
Hypothesis	eliuni.1	$$⊢x=A\to B=C$$
Assertion	eliuni	$$⊢\left(A\in D\wedge E\in C\right)\to E\in \bigcup _{x\in D}B$$

Proof

Step	Hyp	Ref	Expression
1		eliuni.1	$$⊢x=A\to B=C$$
2	1	eleq2d	$$⊢x=A\to \left(E\in B\leftrightarrow E\in C\right)$$
3	2	rspcev	$$⊢\left(A\in D\wedge E\in C\right)\to \exists x\in DE\in B$$
4		eliun	$$⊢E\in \bigcup _{x\in D}B\leftrightarrow \exists x\in DE\in B$$
5	3 4	sylibr	$$⊢\left(A\in D\wedge E\in C\right)\to E\in \bigcup _{x\in D}B$$