Metamath Proof Explorer


Theorem preq12b

Description: Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996)

Ref Expression
Hypotheses preqr1.a 𝐴 ∈ V
preqr1.b 𝐵 ∈ V
preq12b.c 𝐶 ∈ V
preq12b.d 𝐷 ∈ V
Assertion preq12b ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 preqr1.a 𝐴 ∈ V
2 preqr1.b 𝐵 ∈ V
3 preq12b.c 𝐶 ∈ V
4 preq12b.d 𝐷 ∈ V
5 1 prid1 𝐴 ∈ { 𝐴 , 𝐵 }
6 eleq2 ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 ∈ { 𝐴 , 𝐵 } ↔ 𝐴 ∈ { 𝐶 , 𝐷 } ) )
7 5 6 mpbii ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐴 ∈ { 𝐶 , 𝐷 } )
8 1 elpr ( 𝐴 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶𝐴 = 𝐷 ) )
9 7 8 sylib ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶𝐴 = 𝐷 ) )
10 preq1 ( 𝐴 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } )
11 10 eqeq1d ( 𝐴 = 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } ) )
12 2 4 preqr2 ( { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 )
13 11 12 syl6bi ( 𝐴 = 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 ) )
14 13 com12 ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
15 14 ancld ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶 → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
16 prcom { 𝐶 , 𝐷 } = { 𝐷 , 𝐶 }
17 16 eqeq2i ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } )
18 preq1 ( 𝐴 = 𝐷 → { 𝐴 , 𝐵 } = { 𝐷 , 𝐵 } )
19 18 eqeq1d ( 𝐴 = 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } ↔ { 𝐷 , 𝐵 } = { 𝐷 , 𝐶 } ) )
20 2 3 preqr2 ( { 𝐷 , 𝐵 } = { 𝐷 , 𝐶 } → 𝐵 = 𝐶 )
21 19 20 syl6bi ( 𝐴 = 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } → 𝐵 = 𝐶 ) )
22 21 com12 ( { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } → ( 𝐴 = 𝐷𝐵 = 𝐶 ) )
23 17 22 sylbi ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐷𝐵 = 𝐶 ) )
24 23 ancld ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐷 → ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )
25 15 24 orim12d ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ( 𝐴 = 𝐶𝐴 = 𝐷 ) → ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )
26 9 25 mpd ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )
27 preq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
28 preq12 ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } )
29 prcom { 𝐷 , 𝐶 } = { 𝐶 , 𝐷 }
30 28 29 eqtrdi ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
31 27 30 jaoi ( ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
32 26 31 impbii ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )