Metamath Proof Explorer


Theorem unexOLD

Description: Obsolete proof 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 𝐴 ∈ V
unex.2 𝐵 ∈ V
Assertion unexOLD ( 𝐴𝐵 ) ∈ V

Proof

Step Hyp Ref Expression
1 unex.1 𝐴 ∈ V
2 unex.2 𝐵 ∈ V
3 1 2 unipr { 𝐴 , 𝐵 } = ( 𝐴𝐵 )
4 prex { 𝐴 , 𝐵 } ∈ V
5 4 uniex { 𝐴 , 𝐵 } ∈ V
6 3 5 eqeltrri ( 𝐴𝐵 ) ∈ V