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

Metamath Proof Explorer

Theorem iunxsng

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016)

		Ref	Expression
	Hypothesis	iunxsng.1	$⊢ x = A \to B = C$
	Assertion	iunxsng	$⊢ A \in V \to ⋃_{x \in \{A\}} B = C$

Step	Hyp	Ref	Expression
1		iunxsng.1	$⊢ x = A \to B = C$
2		eliun	$⊢ y \in ⋃_{x \in \{A\}} B \leftrightarrow \exists x \in \{A\} y \in B$
3	1	eleq2d	$⊢ x = A \to (y \in B \leftrightarrow y \in C)$
4	3	rexsng	$⊢ A \in V \to (\exists x \in \{A\} y \in B \leftrightarrow y \in C)$
5	2 4	bitrid	$⊢ A \in V \to (y \in ⋃_{x \in \{A\}} B \leftrightarrow y \in C)$
6	5	eqrdv	$⊢ A \in V \to ⋃_{x \in \{A\}} B = C$