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 -> B = C )
Assertion	iunxsng	|- ( A e. V -> U_ x e. { A } B = C )

Proof

Step	Hyp	Ref	Expression
1		iunxsng.1	|- ( x = A -> B = C )
2		eliun	|- ( y e. U_ x e. { A } B <-> E. x e. { A } y e. B )
3	1	eleq2d	|- ( x = A -> ( y e. B <-> y e. C ) )
4	3	rexsng	|- ( A e. V -> ( E. x e. { A } y e. B <-> y e. C ) )
5	2 4	bitrid	|- ( A e. V -> ( y e. U_ x e. { A } B <-> y e. C ) )
6	5	eqrdv	|- ( A e. V -> U_ x e. { A } B = C )