HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-uni 3367
Description: Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16.
Assertion
Ref Expression
df-uni |- U.A = {x | E.y(x e. y /\ y e. A)}
Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-uni
StepHypRef Expression
1 cA . . 3 class A
21cuni 3366 . 2 class U.A
3 vx . . . . . . 7 set x
43cv 1585 . . . . . 6 class x
5 vy . . . . . . 7 set y
65cv 1585 . . . . . 6 class y
74, 6wcel 1588 . . . . 5 wff x e. y
86, 1wcel 1588 . . . . 5 wff y e. A
97, 8wa 337 . . . 4 wff (x e. y /\ y e. A)
109, 5wex 1615 . . 3 wff E.y(x e. y /\ y e. A)
1110, 3cab 2128 . 2 class {x | E.y(x e. y /\ y e. A)}
122, 11wceq 1586 1 wff U.A = {x | E.y(x e. y /\ y e. A)}
Colors of variables: wff set class
This definition is referenced by:  dfuni2 3368  eluni 3369  csbunig 3374  unipr 3380  uniuni 3944  csbunigVD 17556
Copyright terms: Public domain