This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ↔ ∪ 𝐴 = 𝐵 )