Metamath Proof Explorer

Theorem preleqg

Description: Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq . (Contributed by AV, 15-Jun-2022)

Ref Expression
Assertion preleqg ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D ∧ A B = C D → A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 elneq ⊢ A ∈ B → A ≠ B
2 1 3ad2ant1 ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D → A ≠ B
3 preq12nebg ⊢ A ∈ B ∧ B ∈ V ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
4 2 3 syld3an3 ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
5 eleq12 ⊢ A = D ∧ B = C → A ∈ B ↔ D ∈ C
6 elnotel ⊢ D ∈ C → ¬ C ∈ D
7 6 pm2.21d ⊢ D ∈ C → C ∈ D → A = C ∧ B = D
8 5 7 biimtrdi ⊢ A = D ∧ B = C → A ∈ B → C ∈ D → A = C ∧ B = D
9 8 com3l ⊢ A ∈ B → C ∈ D → A = D ∧ B = C → A = C ∧ B = D
10 9 a1d ⊢ A ∈ B → B ∈ V → C ∈ D → A = D ∧ B = C → A = C ∧ B = D
11 10 3imp ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D → A = D ∧ B = C → A = C ∧ B = D
12 11 com12 ⊢ A = D ∧ B = C → A ∈ B ∧ B ∈ V ∧ C ∈ D → A = C ∧ B = D
13 12 jao1i ⊢ A = C ∧ B = D ∨ A = D ∧ B = C → A ∈ B ∧ B ∈ V ∧ C ∈ D → A = C ∧ B = D
14 13 com12 ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D → A = C ∧ B = D ∨ A = D ∧ B = C → A = C ∧ B = D
15 4 14 sylbid ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D → A B = C D → A = C ∧ B = D
16 15 imp ⊢ A ∈ B ∧ B ∈ V ∧ C ∈ D ∧ A B = C D → A = C ∧ B = D