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\to B=C$$
Assertion	iinxsng	$$⊢A\in V\to \bigcap _{x\in \left\{A\right\}}B=C$$

Proof

Step	Hyp	Ref	Expression
1		iinxsng.1	$$⊢x=A\to B=C$$
2		df-iin	$$⊢\bigcap _{x\in \left\{A\right\}}B=\left\{y|\forall x\in \left\{A\right\}y\in B\right\}$$
3	1	eleq2d	$$⊢x=A\to \left(y\in B\leftrightarrow y\in C\right)$$
4	3	ralsng	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}y\in B\leftrightarrow y\in C\right)$$
5	4	eqabcdv	$$⊢A\in V\to \left\{y|\forall x\in \left\{A\right\}y\in B\right\}=C$$
6	2 5	eqtrid	$$⊢A\in V\to \bigcap _{x\in \left\{A\right\}}B=C$$