iunxsngf

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016) (Revised by Thierry Arnoux, 2-May-2020) Avoid ax-13 . (Revised by GG, 19-May-2023)

	Ref	Expression
Hypotheses	iunxsngf.1	$⊢ \underline{Ⅎ} x C$
	iunxsngf.2	$⊢ x = A \to B = C$
Assertion	iunxsngf	$⊢ A \in V \to ⋃_{x \in \{A\}} B = C$

Proof

Step	Hyp	Ref	Expression
1		iunxsngf.1	$⊢ \underline{Ⅎ} x C$
2		iunxsngf.2	$⊢ x = A \to B = C$
3		eliun	$⊢ y \in ⋃_{x \in \{A\}} B \leftrightarrow \exists x \in \{A\} y \in B$
4	1	nfcri	$⊢ Ⅎ x y \in C$
5	2	eleq2d	$⊢ x = A \to (y \in B \leftrightarrow y \in C)$
6	4 5	rexsngf	$⊢ A \in V \to (\exists x \in \{A\} y \in B \leftrightarrow y \in C)$
7	3 6	bitrid	$⊢ A \in V \to (y \in ⋃_{x \in \{A\}} B \leftrightarrow y \in C)$
8	7	eqrdv	$⊢ A \in V \to ⋃_{x \in \{A\}} B = C$

Metamath Proof Explorer

Theorem iunxsngf

Proof