Theorem dfiun2gOLD

Description: Obsolete proof of dfiun2g as of 11-Aug-2023. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dfiun2gOLD	|- ( 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		nfra1	|- F/ x A. x e. A B e. C
2		rsp	|- ( A. x e. A B e. C -> ( x e. A -> B e. C ) )
3		clel3g	|- ( B e. C -> ( z e. B <-> E. y ( y = B /\ z e. y ) ) )
4	2 3	syl6	|- ( A. x e. A B e. C -> ( x e. A -> ( z e. B <-> E. y ( y = B /\ z e. y ) ) ) )
5	4	imp	|- ( ( A. x e. A B e. C /\ x e. A ) -> ( z e. B <-> E. y ( y = B /\ z e. y ) ) )
6	1 5	rexbida	|- ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. x e. A E. y ( y = B /\ z e. y ) ) )
7		rexcom4	|- ( E. x e. A E. y ( y = B /\ z e. y ) <-> E. y E. x e. A ( y = B /\ z e. y ) )
8	6 7	bitrdi	|- ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. y E. x e. A ( y = B /\ z e. y ) ) )
9		r19.41v	|- ( E. x e. A ( y = B /\ z e. y ) <-> ( E. x e. A y = B /\ z e. y ) )
10	9	exbii	|- ( E. y E. x e. A ( y = B /\ z e. y ) <-> E. y ( E. x e. A y = B /\ z e. y ) )
11		exancom	|- ( E. y ( E. x e. A y = B /\ z e. y ) <-> E. y ( z e. y /\ E. x e. A y = B ) )
12	10 11	bitri	|- ( E. y E. x e. A ( y = B /\ z e. y ) <-> E. y ( z e. y /\ E. x e. A y = B ) )
13	8 12	bitrdi	|- ( A. x e. A B e. C -> ( E. x e. A z e. B <-> E. y ( z e. y /\ E. x e. A y = B ) ) )
14		eliun	|- ( z e. U_ x e. A B <-> E. x e. A z e. B )
15		eluniab	|- ( z e. U. { y | E. x e. A y = B } <-> E. y ( z e. y /\ E. x e. A y = B ) )
16	13 14 15	3bitr4g	|- ( A. x e. A B e. C -> ( z e. U_ x e. A B <-> z e. U. { y | E. x e. A y = B } ) )
17	16	eqrdv	|- ( A. x e. A B e. C -> U_ x e. A B = U. { y | E. x e. A y = B } )