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 biimtrdi ⊢ ( 𝐴 = 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → 𝐵 = 𝐷 ) )
14 13 com12 ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶 → 𝐵 = 𝐷 ) )
15 14 ancld ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
16 prcom ⊢ { 𝐶 , 𝐷 } = { 𝐷 , 𝐶 }
17 16 eqeq2i ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } )
18 preq1 ⊢ ( 𝐴 = 𝐷 → { 𝐴 , 𝐵 } = { 𝐷 , 𝐵 } )
19 18 eqeq1d ⊢ ( 𝐴 = 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } ↔ { 𝐷 , 𝐵 } = { 𝐷 , 𝐶 } ) )
20 2 3 preqr2 ⊢ ( { 𝐷 , 𝐵 } = { 𝐷 , 𝐶 } → 𝐵 = 𝐶 )
21 19 20 biimtrdi ⊢ ( 𝐴 = 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } → 𝐵 = 𝐶 ) )
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 ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )