Metamath Proof Explorer

Definition df-iun

Description: Define indexed union. Definition indexed union in Stoll p. 45. In most applications, A is independent of x (although this is not required by the definition), and B depends on x i.e. can be read informally as B ( x ) . We call x the index, A the index set, and B the indexed set. In most books, x e. A is written as a subscript or underneath a union symbol U. . We use a special union symbol U_ to make it easier to distinguish from plain class union. In many theorems, you will see that x and A are in the same distinct variable group (meaning A cannot depend on x ) and that B and x do not share a distinct variable group (meaning that can be thought of as B ( x ) i.e. can be substituted with a class expression containing x ). An alternate definition tying indexed union to ordinary union is dfiun2 . Theorem uniiun provides a definition of ordinary union in terms of indexed union. Theorems fniunfv and funiunfv are useful when B is a function. (Contributed by NM, 27-Jun-1998)

Ref Expression
Assertion df-iun ${⊢}\bigcup _{{x}\in {A}}{B}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}$

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 cA ${class}{A}$
2 cB ${class}{B}$
3 0 1 2 ciun ${class}\bigcup _{{x}\in {A}}{B}$
4 vy ${setvar}{y}$
5 4 cv ${setvar}{y}$
6 5 2 wcel ${wff}{y}\in {B}$
7 6 0 1 wrex ${wff}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
8 7 4 cab ${class}\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}$
9 3 8 wceq ${wff}\bigcup _{{x}\in {A}}{B}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}$