Metamath Proof Explorer


Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

Ref Expression
Assertion iuncom4 𝑥𝐴 𝐵 = 𝑥𝐴 𝐵

Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑧𝐵 𝑦𝑧 ↔ ∃ 𝑧 ( 𝑧𝐵𝑦𝑧 ) )
2 1 rexbii ( ∃ 𝑥𝐴𝑧𝐵 𝑦𝑧 ↔ ∃ 𝑥𝐴𝑧 ( 𝑧𝐵𝑦𝑧 ) )
3 rexcom4 ( ∃ 𝑥𝐴𝑧 ( 𝑧𝐵𝑦𝑧 ) ↔ ∃ 𝑧𝑥𝐴 ( 𝑧𝐵𝑦𝑧 ) )
4 2 3 bitri ( ∃ 𝑥𝐴𝑧𝐵 𝑦𝑧 ↔ ∃ 𝑧𝑥𝐴 ( 𝑧𝐵𝑦𝑧 ) )
5 r19.41v ( ∃ 𝑥𝐴 ( 𝑧𝐵𝑦𝑧 ) ↔ ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
6 5 exbii ( ∃ 𝑧𝑥𝐴 ( 𝑧𝐵𝑦𝑧 ) ↔ ∃ 𝑧 ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
7 4 6 bitri ( ∃ 𝑥𝐴𝑧𝐵 𝑦𝑧 ↔ ∃ 𝑧 ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
8 eluni2 ( 𝑦 𝐵 ↔ ∃ 𝑧𝐵 𝑦𝑧 )
9 8 rexbii ( ∃ 𝑥𝐴 𝑦 𝐵 ↔ ∃ 𝑥𝐴𝑧𝐵 𝑦𝑧 )
10 df-rex ( ∃ 𝑧 𝑥𝐴 𝐵 𝑦𝑧 ↔ ∃ 𝑧 ( 𝑧 𝑥𝐴 𝐵𝑦𝑧 ) )
11 eliun ( 𝑧 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴 𝑧𝐵 )
12 11 anbi1i ( ( 𝑧 𝑥𝐴 𝐵𝑦𝑧 ) ↔ ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
13 12 exbii ( ∃ 𝑧 ( 𝑧 𝑥𝐴 𝐵𝑦𝑧 ) ↔ ∃ 𝑧 ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
14 10 13 bitri ( ∃ 𝑧 𝑥𝐴 𝐵 𝑦𝑧 ↔ ∃ 𝑧 ( ∃ 𝑥𝐴 𝑧𝐵𝑦𝑧 ) )
15 7 9 14 3bitr4i ( ∃ 𝑥𝐴 𝑦 𝐵 ↔ ∃ 𝑧 𝑥𝐴 𝐵 𝑦𝑧 )
16 eliun ( 𝑦 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴 𝑦 𝐵 )
17 eluni2 ( 𝑦 𝑥𝐴 𝐵 ↔ ∃ 𝑧 𝑥𝐴 𝐵 𝑦𝑧 )
18 15 16 17 3bitr4i ( 𝑦 𝑥𝐴 𝐵𝑦 𝑥𝐴 𝐵 )
19 18 eqriv 𝑥𝐴 𝐵 = 𝑥𝐴 𝐵