Metamath Proof Explorer

Theorem preleqALT

Description: Alternate proof of preleq , not based on preleqg : Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses preleq.b ⊢B∈V
preleqALT.d ⊢D∈V
Assertion preleqALT ⊢A∈B∧C∈D∧AB=CD→A=C∧B=D

Proof

Step Hyp Ref Expression
1 preleq.b ⊢B∈V
2 preleqALT.d ⊢D∈V
3 1 jctr ⊢A∈B→A∈B∧B∈V
4 2 jctr ⊢C∈D→C∈D∧D∈V
5 preq12bg ⊢A∈B∧B∈V∧C∈D∧D∈V→AB=CD↔A=C∧B=D∨A=D∧B=C
6 3 4 5 syl2an ⊢A∈B∧C∈D→AB=CD↔A=C∧B=D∨A=D∧B=C
7 6 biimpa ⊢A∈B∧C∈D∧AB=CD→A=C∧B=D∨A=D∧B=C
8 7 ord ⊢A∈B∧C∈D∧AB=CD→¬A=C∧B=D→A=D∧B=C
9 en2lp ⊢¬D∈C∧C∈D
10 eleq12 ⊢A=D∧B=C→A∈B↔D∈C
11 10 anbi1d ⊢A=D∧B=C→A∈B∧C∈D↔D∈C∧C∈D
12 9 11 mtbiri ⊢A=D∧B=C→¬A∈B∧C∈D
13 8 12 syl6 ⊢A∈B∧C∈D∧AB=CD→¬A=C∧B=D→¬A∈B∧C∈D
14 13 con4d ⊢A∈B∧C∈D∧AB=CD→A∈B∧C∈D→A=C∧B=D
15 14 ex ⊢A∈B∧C∈D→AB=CD→A∈B∧C∈D→A=C∧B=D
16 15 pm2.43a ⊢A∈B∧C∈D→AB=CD→A=C∧B=D
17 16 imp ⊢A∈B∧C∈D∧AB=CD→A=C∧B=D