Metamath Proof Explorer


Theorem inuni

Description: The intersection of a union U. A with a class B is equal to the union of the intersections of each element of A with B . (Contributed by FL, 24-Mar-2007) (Proof shortened by Wolf Lammen, 15-May-2025)

Ref Expression
Assertion inuni ( 𝐴𝐵 ) = { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) }

Proof

Step Hyp Ref Expression
1 ancom ( ( 𝑧𝑥 ∧ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ) ↔ ( ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
2 r19.41v ( ∃ 𝑦𝐴 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) ↔ ( ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
3 1 2 bitr4i ( ( 𝑧𝑥 ∧ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ) ↔ ∃ 𝑦𝐴 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
4 3 exbii ( ∃ 𝑥 ( 𝑧𝑥 ∧ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ) ↔ ∃ 𝑥𝑦𝐴 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
5 eluniab ( 𝑧 { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) } ↔ ∃ 𝑥 ( 𝑧𝑥 ∧ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) ) )
6 eluni2 ( 𝑧 𝐴 ↔ ∃ 𝑦𝐴 𝑧𝑦 )
7 6 anbi1i ( ( 𝑧 𝐴𝑧𝐵 ) ↔ ( ∃ 𝑦𝐴 𝑧𝑦𝑧𝐵 ) )
8 elin ( 𝑧 ∈ ( 𝐴𝐵 ) ↔ ( 𝑧 𝐴𝑧𝐵 ) )
9 r19.41v ( ∃ 𝑦𝐴 ( 𝑧𝑦𝑧𝐵 ) ↔ ( ∃ 𝑦𝐴 𝑧𝑦𝑧𝐵 ) )
10 7 8 9 3bitr4i ( 𝑧 ∈ ( 𝐴𝐵 ) ↔ ∃ 𝑦𝐴 ( 𝑧𝑦𝑧𝐵 ) )
11 vex 𝑦 ∈ V
12 11 inex1 ( 𝑦𝐵 ) ∈ V
13 eleq2 ( 𝑥 = ( 𝑦𝐵 ) → ( 𝑧𝑥𝑧 ∈ ( 𝑦𝐵 ) ) )
14 12 13 ceqsexv ( ∃ 𝑥 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) ↔ 𝑧 ∈ ( 𝑦𝐵 ) )
15 elin ( 𝑧 ∈ ( 𝑦𝐵 ) ↔ ( 𝑧𝑦𝑧𝐵 ) )
16 14 15 bitri ( ∃ 𝑥 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) ↔ ( 𝑧𝑦𝑧𝐵 ) )
17 16 rexbii ( ∃ 𝑦𝐴𝑥 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) ↔ ∃ 𝑦𝐴 ( 𝑧𝑦𝑧𝐵 ) )
18 rexcom4 ( ∃ 𝑦𝐴𝑥 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) ↔ ∃ 𝑥𝑦𝐴 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
19 10 17 18 3bitr2i ( 𝑧 ∈ ( 𝐴𝐵 ) ↔ ∃ 𝑥𝑦𝐴 ( 𝑥 = ( 𝑦𝐵 ) ∧ 𝑧𝑥 ) )
20 4 5 19 3bitr4ri ( 𝑧 ∈ ( 𝐴𝐵 ) ↔ 𝑧 { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) } )
21 20 eqriv ( 𝐴𝐵 ) = { 𝑥 ∣ ∃ 𝑦𝐴 𝑥 = ( 𝑦𝐵 ) }