Theorem brbigcup

Description: Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Hypothesis	brbigcup.1	|- B e. _V
Assertion	brbigcup	|- ( A Bigcup B <-> U. A = B )

Proof

Step	Hyp	Ref	Expression
1		brbigcup.1	|- B e. _V
2		relbigcup	|- Rel Bigcup
3	2	brrelex1i	|- ( A Bigcup B -> A e. _V )
4		eleq1	|- ( U. A = B -> ( U. A e. _V <-> B e. _V ) )
5	1 4	mpbiri	|- ( U. A = B -> U. A e. _V )
6		uniexb	|- ( A e. _V <-> U. A e. _V )
7	5 6	sylibr	|- ( U. A = B -> A e. _V )
8		breq1	|- ( x = A -> ( x Bigcup B <-> A Bigcup B ) )
9		unieq	|- ( x = A -> U. x = U. A )
10	9	eqeq1d	|- ( x = A -> ( U. x = B <-> U. A = B ) )
11		vex	|- x e. _V
12		df-bigcup	|- Bigcup = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) )
13		brxp	|- ( x ( _V X. _V ) B <-> ( x e. _V /\ B e. _V ) )
14	11 1 13	mpbir2an	|- x ( _V X. _V ) B
15		epel	|- ( y _E z <-> y e. z )
16	15	rexbii	|- ( E. z e. x y _E z <-> E. z e. x y e. z )
17		vex	|- y e. _V
18	17 11	coep	|- ( y ( _E o. _E ) x <-> E. z e. x y _E z )
19		eluni2	|- ( y e. U. x <-> E. z e. x y e. z )
20	16 18 19	3bitr4ri	|- ( y e. U. x <-> y ( _E o. _E ) x )
21	11 1 12 14 20	brtxpsd3	|- ( x Bigcup B <-> B = U. x )
22		eqcom	|- ( B = U. x <-> U. x = B )
23	21 22	bitri	|- ( x Bigcup B <-> U. x = B )
24	8 10 23	vtoclbg	|- ( A e. _V -> ( A Bigcup B <-> U. A = B ) )
25	3 7 24	pm5.21nii	|- ( A Bigcup B <-> U. A = B )