Theorem iinxsng

Description: A singleton index picks out an instance of an indexed intersection's argument. (Contributed by NM, 15-Jan-2012) (Proof shortened by Mario Carneiro, 17-Nov-2016)

	Ref	Expression
Hypothesis	iinxsng.1	|- ( x = A -> B = C )
Assertion	iinxsng	|- ( A e. V -> |^|_ x e. { A } B = C )

Proof

Step	Hyp	Ref	Expression
1		iinxsng.1	|- ( x = A -> B = C )
2		df-iin	|- |^|_ x e. { A } B = { y | A. x e. { A } y e. B }
3	1	eleq2d	|- ( x = A -> ( y e. B <-> y e. C ) )
4	3	ralsng	|- ( A e. V -> ( A. x e. { A } y e. B <-> y e. C ) )
5	4	abbi1dv	|- ( A e. V -> { y | A. x e. { A } y e. B } = C )
6	2 5	eqtrid	|- ( A e. V -> |^|_ x e. { A } B = C )