This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = A \to B = C$
	Assertion	eliuni	$⊢ (A \in D \land E \in C) \to E \in ⋃_{x \in D} B$

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