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 A B = x | y A x = y B

Proof

Step Hyp Ref Expression
1 ancom z x y A x = y B y A x = y B z x
2 r19.41v y A x = y B z x y A x = y B z x
3 1 2 bitr4i z x y A x = y B y A x = y B z x
4 3 exbii x z x y A x = y B x y A x = y B z x
5 eluniab z x | y A x = y B x z x y A x = y B
6 eluni2 z A y A z y
7 6 anbi1i z A z B y A z y z B
8 elin z A B z A z B
9 r19.41v y A z y z B y A z y z B
10 7 8 9 3bitr4i z A B y A z y z B
11 vex y V
12 11 inex1 y B V
13 eleq2 x = y B z x z y B
14 12 13 ceqsexv x x = y B z x z y B
15 elin z y B z y z B
16 14 15 bitri x x = y B z x z y z B
17 16 rexbii y A x x = y B z x y A z y z B
18 rexcom4 y A x x = y B z x x y A x = y B z x
19 10 17 18 3bitr2i z A B x y A x = y B z x
20 4 5 19 3bitr4ri z A B z x | y A x = y B
21 20 eqriv A B = x | y A x = y B