Metamath Proof Explorer


Theorem uniprgOLD

Description: Obsolete version of unipr as of 1-Sep-2024. (Contributed by NM, 25-Aug-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion uniprgOLD ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 preq1 ( 𝑥 = 𝐴 → { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
2 1 unieqd ( 𝑥 = 𝐴 { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
3 uneq1 ( 𝑥 = 𝐴 → ( 𝑥𝑦 ) = ( 𝐴𝑦 ) )
4 2 3 eqeq12d ( 𝑥 = 𝐴 → ( { 𝑥 , 𝑦 } = ( 𝑥𝑦 ) ↔ { 𝐴 , 𝑦 } = ( 𝐴𝑦 ) ) )
5 preq2 ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
6 5 unieqd ( 𝑦 = 𝐵 { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
7 uneq2 ( 𝑦 = 𝐵 → ( 𝐴𝑦 ) = ( 𝐴𝐵 ) )
8 6 7 eqeq12d ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } = ( 𝐴𝑦 ) ↔ { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) ) )
9 vex 𝑥 ∈ V
10 vex 𝑦 ∈ V
11 9 10 unipr { 𝑥 , 𝑦 } = ( 𝑥𝑦 )
12 4 8 11 vtocl2g ( ( 𝐴𝑉𝐵𝑊 ) → { 𝐴 , 𝐵 } = ( 𝐴𝐵 ) )