This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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