Metamath Proof Explorer


Theorem unipr

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 AV
unipr.2 BV
Assertion unipr AB=AB

Proof

Step Hyp Ref Expression
1 unipr.1 AV
2 unipr.2 BV
3 uniprg AVBVAB=AB
4 1 2 3 mp2an AB=AB