| Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Extend class notation to include the union of a class (read: 'union A ') |
| Ref | Expression |
|---|---|
| cA | class A |
| Ref | Expression |
|---|---|
| cuni | class ∪A |
| Colors of variables: wff set class |