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

Metamath Proof Explorer

Theorem unexOLD

Description: Obsolete version of unex as of 21-Jul-2025. (Contributed by NM, 1-Jul-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses unex.1 ⊢ A ∈ V
unex.2 ⊢ B ∈ V
Assertion unexOLD ⊢ A ∪ B ∈ V

Proof

Step Hyp Ref Expression
1 unex.1 ⊢ A ∈ V
2 unex.2 ⊢ B ∈ V
3 1 2 unipr ⊢ ⋃ A B = A ∪ B
4 prex ⊢ A B ∈ V
5 4 uniex ⊢ ⋃ A B ∈ V
6 3 5 eqeltrri ⊢ A ∪ B ∈ V