Metamath Proof Explorer


Theorem uniuni

Description: Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007)

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

Proof

Step Hyp Ref Expression
1 eluni ( 𝑢 𝐴 ↔ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) )
2 1 anbi2i ( ( 𝑧𝑢𝑢 𝐴 ) ↔ ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) )
3 2 exbii ( ∃ 𝑢 ( 𝑧𝑢𝑢 𝐴 ) ↔ ∃ 𝑢 ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) )
4 19.42v ( ∃ 𝑦 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) ↔ ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) )
5 4 bicomi ( ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑦 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) )
6 5 exbii ( ∃ 𝑢 ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑢𝑦 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) )
7 excom ( ∃ 𝑢𝑦 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑦𝑢 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) )
8 anass ( ( ( 𝑧𝑢𝑢𝑦 ) ∧ 𝑦𝐴 ) ↔ ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) )
9 ancom ( ( ( 𝑧𝑢𝑢𝑦 ) ∧ 𝑦𝐴 ) ↔ ( 𝑦𝐴 ∧ ( 𝑧𝑢𝑢𝑦 ) ) )
10 8 9 bitr3i ( ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) ↔ ( 𝑦𝐴 ∧ ( 𝑧𝑢𝑢𝑦 ) ) )
11 10 2exbii ( ∃ 𝑦𝑢 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑦𝑢 ( 𝑦𝐴 ∧ ( 𝑧𝑢𝑢𝑦 ) ) )
12 exdistr ( ∃ 𝑦𝑢 ( 𝑦𝐴 ∧ ( 𝑧𝑢𝑢𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦𝐴 ∧ ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) ) )
13 7 11 12 3bitri ( ∃ 𝑢𝑦 ( 𝑧𝑢 ∧ ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦𝐴 ∧ ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) ) )
14 eluni ( 𝑧 𝑦 ↔ ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) )
15 14 bicomi ( ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) ↔ 𝑧 𝑦 )
16 15 anbi2i ( ( 𝑦𝐴 ∧ ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) ) ↔ ( 𝑦𝐴𝑧 𝑦 ) )
17 16 exbii ( ∃ 𝑦 ( 𝑦𝐴 ∧ ∃ 𝑢 ( 𝑧𝑢𝑢𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦𝐴𝑧 𝑦 ) )
18 6 13 17 3bitri ( ∃ 𝑢 ( 𝑧𝑢 ∧ ∃ 𝑦 ( 𝑢𝑦𝑦𝐴 ) ) ↔ ∃ 𝑦 ( 𝑦𝐴𝑧 𝑦 ) )
19 vuniex 𝑦 ∈ V
20 eleq2 ( 𝑣 = 𝑦 → ( 𝑧𝑣𝑧 𝑦 ) )
21 19 20 ceqsexv ( ∃ 𝑣 ( 𝑣 = 𝑦𝑧𝑣 ) ↔ 𝑧 𝑦 )
22 exancom ( ∃ 𝑣 ( 𝑣 = 𝑦𝑧𝑣 ) ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 = 𝑦 ) )
23 21 22 bitr3i ( 𝑧 𝑦 ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 = 𝑦 ) )
24 23 anbi2i ( ( 𝑦𝐴𝑧 𝑦 ) ↔ ( 𝑦𝐴 ∧ ∃ 𝑣 ( 𝑧𝑣𝑣 = 𝑦 ) ) )
25 19.42v ( ∃ 𝑣 ( 𝑦𝐴 ∧ ( 𝑧𝑣𝑣 = 𝑦 ) ) ↔ ( 𝑦𝐴 ∧ ∃ 𝑣 ( 𝑧𝑣𝑣 = 𝑦 ) ) )
26 ancom ( ( 𝑦𝐴 ∧ ( 𝑧𝑣𝑣 = 𝑦 ) ) ↔ ( ( 𝑧𝑣𝑣 = 𝑦 ) ∧ 𝑦𝐴 ) )
27 anass ( ( ( 𝑧𝑣𝑣 = 𝑦 ) ∧ 𝑦𝐴 ) ↔ ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
28 26 27 bitri ( ( 𝑦𝐴 ∧ ( 𝑧𝑣𝑣 = 𝑦 ) ) ↔ ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
29 28 exbii ( ∃ 𝑣 ( 𝑦𝐴 ∧ ( 𝑧𝑣𝑣 = 𝑦 ) ) ↔ ∃ 𝑣 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
30 24 25 29 3bitr2i ( ( 𝑦𝐴𝑧 𝑦 ) ↔ ∃ 𝑣 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
31 30 exbii ( ∃ 𝑦 ( 𝑦𝐴𝑧 𝑦 ) ↔ ∃ 𝑦𝑣 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
32 excom ( ∃ 𝑦𝑣 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) ↔ ∃ 𝑣𝑦 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
33 exdistr ( ∃ 𝑣𝑦 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧𝑣 ∧ ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) ) )
34 vex 𝑣 ∈ V
35 eqeq1 ( 𝑥 = 𝑣 → ( 𝑥 = 𝑦𝑣 = 𝑦 ) )
36 35 anbi1d ( 𝑥 = 𝑣 → ( ( 𝑥 = 𝑦𝑦𝐴 ) ↔ ( 𝑣 = 𝑦𝑦𝐴 ) ) )
37 36 exbidv ( 𝑥 = 𝑣 → ( ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) ↔ ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) ) )
38 34 37 elab ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ↔ ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) )
39 38 bicomi ( ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) ↔ 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } )
40 39 anbi2i ( ( 𝑧𝑣 ∧ ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) ) ↔ ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) )
41 40 exbii ( ∃ 𝑣 ( 𝑧𝑣 ∧ ∃ 𝑦 ( 𝑣 = 𝑦𝑦𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) )
42 33 41 bitri ( ∃ 𝑣𝑦 ( 𝑧𝑣 ∧ ( 𝑣 = 𝑦𝑦𝐴 ) ) ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) )
43 31 32 42 3bitri ( ∃ 𝑦 ( 𝑦𝐴𝑧 𝑦 ) ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) )
44 3 18 43 3bitri ( ∃ 𝑢 ( 𝑧𝑢𝑢 𝐴 ) ↔ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) )
45 44 abbii { 𝑧 ∣ ∃ 𝑢 ( 𝑧𝑢𝑢 𝐴 ) } = { 𝑧 ∣ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) }
46 df-uni 𝐴 = { 𝑧 ∣ ∃ 𝑢 ( 𝑧𝑢𝑢 𝐴 ) }
47 df-uni { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } = { 𝑧 ∣ ∃ 𝑣 ( 𝑧𝑣𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) } ) }
48 45 46 47 3eqtr4i 𝐴 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = 𝑦𝑦𝐴 ) }