Metamath Proof Explorer


Theorem bj-restuni

Description: The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restuni X V A W X 𝑡 A = X A

Proof

Step Hyp Ref Expression
1 eluni x X 𝑡 A y x y y X 𝑡 A
2 elrest X V A W y X 𝑡 A z X y = z A
3 2 anbi2d X V A W x y y X 𝑡 A x y z X y = z A
4 3 exbidv X V A W y x y y X 𝑡 A y x y z X y = z A
5 eluni x X z x z z X
6 5 bicomi z x z z X x X
7 6 anbi1i z x z z X x A x X x A
8 7 a1i X V A W z x z z X x A x X x A
9 df-rex z X y = z A z z X y = z A
10 9 anbi2i x y z X y = z A x y z z X y = z A
11 19.42v z x y z X y = z A x y z z X y = z A
12 11 bicomi x y z z X y = z A z x y z X y = z A
13 10 12 bitri x y z X y = z A z x y z X y = z A
14 13 exbii y x y z X y = z A y z x y z X y = z A
15 excom y z x y z X y = z A z y x y z X y = z A
16 an12 x y z X y = z A z X x y y = z A
17 16 exbii y x y z X y = z A y z X x y y = z A
18 19.42v y z X x y y = z A z X y x y y = z A
19 eqimss y = z A y z A
20 19 sseld y = z A x y x z A
21 20 imdistanri x y y = z A x z A y = z A
22 eqimss2 y = z A z A y
23 22 sseld y = z A x z A x y
24 23 imdistanri x z A y = z A x y y = z A
25 21 24 impbii x y y = z A x z A y = z A
26 25 exbii y x y y = z A y x z A y = z A
27 19.42v y x z A y = z A x z A y y = z A
28 vex z V
29 28 inex1 z A V
30 29 isseti y y = z A
31 30 biantru x z A x z A y y = z A
32 31 bicomi x z A y y = z A x z A
33 elin x z A x z x A
34 32 33 bitri x z A y y = z A x z x A
35 26 27 34 3bitri y x y y = z A x z x A
36 35 bianassc z X y x y y = z A x z z X x A
37 17 18 36 3bitri y x y z X y = z A x z z X x A
38 37 exbii z y x y z X y = z A z x z z X x A
39 19.41v z x z z X x A z x z z X x A
40 38 39 bitri z y x y z X y = z A z x z z X x A
41 14 15 40 3bitri y x y z X y = z A z x z z X x A
42 elin x X A x X x A
43 8 41 42 3bitr4g X V A W y x y z X y = z A x X A
44 4 43 bitrd X V A W y x y y X 𝑡 A x X A
45 1 44 syl5bb X V A W x X 𝑡 A x X A
46 45 eqrdv X V A W X 𝑡 A = X A