Metamath Proof Explorer


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 syl5bb
 |-  ( 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 )