Theorem 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 Gino Giotto, 19-May-2023)

	Ref	Expression
Hypotheses	iunxsngf.1	|- F/_ x C
	iunxsngf.2	|- ( x = A -> B = C )
Assertion	iunxsngf	|- ( A e. V -> U_ x e. { A } B = C )

Proof

Step	Hyp	Ref	Expression
1		iunxsngf.1	|- F/_ x C
2		iunxsngf.2	|- ( x = A -> B = C )
3		eliun	|- ( y e. U_ x e. { A } B <-> E. x e. { A } y e. B )
4	1	nfcri	|- F/ x y e. C
5	2	eleq2d	|- ( x = A -> ( y e. B <-> y e. C ) )
6	4 5	rexsngf	|- ( A e. V -> ( E. x e. { A } y e. B <-> y e. C ) )
7	3 6	bitrid	|- ( A e. V -> ( y e. U_ x e. { A } B <-> y e. C ) )
8	7	eqrdv	|- ( A e. V -> U_ x e. { A } B = C )