Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 23-Aug-1993) (Proof shortened by BJ, 1-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | unipr.1 | |- A e. _V |
|
| unipr.2 | |- B e. _V |
||
| Assertion | unipr | |- U. { A , B } = ( A u. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unipr.1 | |- A e. _V |
|
| 2 | unipr.2 | |- B e. _V |
|
| 3 | uniprg | |- ( ( A e. _V /\ B e. _V ) -> U. { A , B } = ( A u. B ) ) |
|
| 4 | 1 2 3 | mp2an | |- U. { A , B } = ( A u. B ) |