Theorem brbigcup

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

	Ref	Expression
Hypothesis	brbigcup.1	⊢ 𝐵 ∈ V
Assertion	brbigcup	⊢ ( 𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		brbigcup.1	⊢ 𝐵 ∈ V
2		relbigcup	⊢ Rel Bigcup
3	2	brrelex1i	⊢ ( 𝐴 Bigcup 𝐵 → 𝐴 ∈ V )
4		eleq1	⊢ ( ∪ 𝐴 = 𝐵 → ( ∪ 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
5	1 4	mpbiri	⊢ ( ∪ 𝐴 = 𝐵 → ∪ 𝐴 ∈ V )
6		uniexb	⊢ ( 𝐴 ∈ V ↔ ∪ 𝐴 ∈ V )
7	5 6	sylibr	⊢ ( ∪ 𝐴 = 𝐵 → 𝐴 ∈ V )
8		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 Bigcup 𝐵 ↔ 𝐴 Bigcup 𝐵 ) )
9		unieq	⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
10	9	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 = 𝐵 ↔ ∪ 𝐴 = 𝐵 ) )
11		vex	⊢ 𝑥 ∈ V
12		df-bigcup	⊢ Bigcup = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) )
13		brxp	⊢ ( 𝑥 ( V × V ) 𝐵 ↔ ( 𝑥 ∈ V ∧ 𝐵 ∈ V ) )
14	11 1 13	mpbir2an	⊢ 𝑥 ( V × V ) 𝐵
15		epel	⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
16	15	rexbii	⊢ ( ∃ 𝑧 ∈ 𝑥 𝑦 E 𝑧 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ∈ 𝑧 )
17		vex	⊢ 𝑦 ∈ V
18	17 11	coep	⊢ ( 𝑦 ( E ∘ E ) 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 E 𝑧 )
19		eluni2	⊢ ( 𝑦 ∈ ∪ 𝑥 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ∈ 𝑧 )
20	16 18 19	3bitr4ri	⊢ ( 𝑦 ∈ ∪ 𝑥 ↔ 𝑦 ( E ∘ E ) 𝑥 )
21	11 1 12 14 20	brtxpsd3	⊢ ( 𝑥 Bigcup 𝐵 ↔ 𝐵 = ∪ 𝑥 )
22		eqcom	⊢ ( 𝐵 = ∪ 𝑥 ↔ ∪ 𝑥 = 𝐵 )
23	21 22	bitri	⊢ ( 𝑥 Bigcup 𝐵 ↔ ∪ 𝑥 = 𝐵 )
24	8 10 23	vtoclbg	⊢ ( 𝐴 ∈ V → ( 𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵 ) )
25	3 7 24	pm5.21nii	⊢ ( 𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵 )