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) Avoid ax-10 , ax-12 . (Revised by SN, 11-Dec-2024)

	Ref	Expression
Assertion	dfiun2g	|- ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )

Proof

Step	Hyp	Ref	Expression
1		df-iun	|- U_ x e. A B = { z | E. x e. A z e. B }
2		elisset	|- ( B e. C -> E. z z = B )
3		eleq2	|- ( z = B -> ( w e. z <-> w e. B ) )
4	3	pm5.32ri	|- ( ( w e. z /\ z = B ) <-> ( w e. B /\ z = B ) )
5	4	simplbi2	|- ( w e. B -> ( z = B -> ( w e. z /\ z = B ) ) )
6	5	eximdv	|- ( w e. B -> ( E. z z = B -> E. z ( w e. z /\ z = B ) ) )
7	2 6	syl5com	|- ( B e. C -> ( w e. B -> E. z ( w e. z /\ z = B ) ) )
8	7	ralimi	|- ( A. x e. A B e. C -> A. x e. A ( w e. B -> E. z ( w e. z /\ z = B ) ) )
9		rexim	|- ( A. x e. A ( w e. B -> E. z ( w e. z /\ z = B ) ) -> ( E. x e. A w e. B -> E. x e. A E. z ( w e. z /\ z = B ) ) )
10	8 9	syl	|- ( A. x e. A B e. C -> ( E. x e. A w e. B -> E. x e. A E. z ( w e. z /\ z = B ) ) )
11		rexcom4	|- ( E. x e. A E. z ( w e. z /\ z = B ) <-> E. z E. x e. A ( w e. z /\ z = B ) )
12		r19.42v	|- ( E. x e. A ( w e. z /\ z = B ) <-> ( w e. z /\ E. x e. A z = B ) )
13	12	exbii	|- ( E. z E. x e. A ( w e. z /\ z = B ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
14	11 13	bitri	|- ( E. x e. A E. z ( w e. z /\ z = B ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
15	10 14	imbitrdi	|- ( A. x e. A B e. C -> ( E. x e. A w e. B -> E. z ( w e. z /\ E. x e. A z = B ) ) )
16	3	biimpac	|- ( ( w e. z /\ z = B ) -> w e. B )
17	16	reximi	|- ( E. x e. A ( w e. z /\ z = B ) -> E. x e. A w e. B )
18	12 17	sylbir	|- ( ( w e. z /\ E. x e. A z = B ) -> E. x e. A w e. B )
19	18	exlimiv	|- ( E. z ( w e. z /\ E. x e. A z = B ) -> E. x e. A w e. B )
20	15 19	impbid1	|- ( A. x e. A B e. C -> ( E. x e. A w e. B <-> E. z ( w e. z /\ E. x e. A z = B ) ) )
21		vex	|- w e. _V
22		eleq1w	|- ( z = w -> ( z e. B <-> w e. B ) )
23	22	rexbidv	|- ( z = w -> ( E. x e. A z e. B <-> E. x e. A w e. B ) )
24	21 23	elab	|- ( w e. { z | E. x e. A z e. B } <-> E. x e. A w e. B )
25		eluni	|- ( w e. U. { y | E. x e. A y = B } <-> E. z ( w e. z /\ z e. { y | E. x e. A y = B } ) )
26		vex	|- z e. _V
27		eqeq1	|- ( y = z -> ( y = B <-> z = B ) )
28	27	rexbidv	|- ( y = z -> ( E. x e. A y = B <-> E. x e. A z = B ) )
29	26 28	elab	|- ( z e. { y | E. x e. A y = B } <-> E. x e. A z = B )
30	29	anbi2i	|- ( ( w e. z /\ z e. { y | E. x e. A y = B } ) <-> ( w e. z /\ E. x e. A z = B ) )
31	30	exbii	|- ( E. z ( w e. z /\ z e. { y | E. x e. A y = B } ) <-> E. z ( w e. z /\ E. x e. A z = B ) )
32	25 31	bitri	|- ( w e. U. { y | E. x e. A y = B } <-> E. z ( w e. z /\ E. x e. A z = B ) )
33	20 24 32	3bitr4g	|- ( A. x e. A B e. C -> ( w e. { z | E. x e. A z e. B } <-> w e. U. { y | E. x e. A y = B } ) )
34	33	eqrdv	|- ( A. x e. A B e. C -> { z | E. x e. A z e. B } = U. { y | E. x e. A y = B } )
35	1 34	eqtrid	|- ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )