Metamath Proof Explorer

Theorem prel12g

Description: Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996) (Revised by AV, 9-Dec-2018) (Revised by AV, 12-Jun-2022)

Ref Expression
Assertion prel12g ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )

Proof

Step Hyp Ref Expression
1 preq12nebg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
2 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐷 } )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ { 𝐴 , 𝐷 } )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ { 𝐴 , 𝐷 } )
5 preq1 ⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝐷 } = { 𝐶 , 𝐷 } )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 = 𝐶 ) → { 𝐴 , 𝐷 } = { 𝐶 , 𝐷 } )
7 4 6 eleqtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ { 𝐶 , 𝐷 } )
8 7 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐶 → 𝐴 ∈ { 𝐶 , 𝐷 } ) )
9 prid2g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐶 , 𝐵 } )
10 9 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ { 𝐶 , 𝐵 } )
11 preq2 ⊢ ( 𝐵 = 𝐷 → { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } )
12 11 eleq2d ⊢ ( 𝐵 = 𝐷 → ( 𝐵 ∈ { 𝐶 , 𝐵 } ↔ 𝐵 ∈ { 𝐶 , 𝐷 } ) )
13 10 12 syl5ibcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 = 𝐷 → 𝐵 ∈ { 𝐶 , 𝐷 } ) )
14 8 13 anim12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )
15 prid2g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐶 , 𝐴 } )
16 15 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ { 𝐶 , 𝐴 } )
17 preq2 ⊢ ( 𝐴 = 𝐷 → { 𝐶 , 𝐴 } = { 𝐶 , 𝐷 } )
18 17 eleq2d ⊢ ( 𝐴 = 𝐷 → ( 𝐴 ∈ { 𝐶 , 𝐴 } ↔ 𝐴 ∈ { 𝐶 , 𝐷 } ) )
19 16 18 syl5ibcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 = 𝐷 → 𝐴 ∈ { 𝐶 , 𝐷 } ) )
20 prid1g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 , 𝐷 } )
21 20 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ { 𝐵 , 𝐷 } )
22 preq1 ⊢ ( 𝐵 = 𝐶 → { 𝐵 , 𝐷 } = { 𝐶 , 𝐷 } )
23 22 eleq2d ⊢ ( 𝐵 = 𝐶 → ( 𝐵 ∈ { 𝐵 , 𝐷 } ↔ 𝐵 ∈ { 𝐶 , 𝐷 } ) )
24 21 23 syl5ibcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 = 𝐶 → 𝐵 ∈ { 𝐶 , 𝐷 } ) )
25 19 24 anim12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )
26 14 25 jaod ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )
27 elprg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )
28 27 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )
29 elprg ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
30 29 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
31 28 30 anbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )
32 eqtr3 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
33 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
34 32 33 syl ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
35 olc ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
36 35 a1d ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
37 orc ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
38 37 a1d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
39 eqtr3 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → 𝐴 = 𝐵 )
40 39 33 syl ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
41 34 36 38 40 ccase ⊢ ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
42 41 com12 ⊢ ( 𝐴 ≠ 𝐵 → ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
43 42 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
44 31 43 sylbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
45 26 44 impbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ↔ ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )
46 1 45 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ) )