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 A V
unipr.2 B V
Assertion unipr A B = A B

Proof

Step Hyp Ref Expression
1 unipr.1 A V
2 unipr.2 B V
3 uniprg A V B V A B = A B
4 1 2 3 mp2an A B = A B