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∧AB=CD→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→AB=CD↔A=C∧B=D∨A=D∧B=C
4 2 3 syld3an3 ⊢A∈B∧B∈V∧C∈D→AB=CD↔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 syl6bi ⊢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→AB=CD→A=C∧B=D
16 15 imp ⊢A∈B∧B∈V∧C∈D∧AB=CD→A=C∧B=D