Metamath Proof Explorer


Theorem dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Assertion dfiun2g x A B C x A B = y | x A y = B

Proof

Step Hyp Ref Expression
1 nfra1 x x A B C
2 rspa x A B C x A B C
3 clel3g B C z B y y = B z y
4 2 3 syl x A B C x A z B y y = B z y
5 1 4 rexbida x A B C x A z B x A y y = B z y
6 rexcom4 x A y y = B z y y x A y = B z y
7 5 6 bitrdi x A B C x A z B y x A y = B z y
8 r19.41v x A y = B z y x A y = B z y
9 8 exbii y x A y = B z y y x A y = B z y
10 exancom y x A y = B z y y z y x A y = B
11 9 10 bitri y x A y = B z y y z y x A y = B
12 7 11 bitrdi x A B C x A z B y z y x A y = B
13 eliun z x A B x A z B
14 eluniab z y | x A y = B y z y x A y = B
15 12 13 14 3bitr4g x A B C z x A B z y | x A y = B
16 15 eqrdv x A B C x A B = y | x A y = B