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 A B = C D 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 A B = C D A = C B = D A = D B = C
6 3 4 5 syl2an A B C D A B = C D A = C B = D A = D B = C
7 6 biimpa A B C D A B = C D A = C B = D A = D B = C
8 7 ord A B C D A B = C D ¬ 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 A B = C D ¬ A = C B = D ¬ A B C D
14 13 con4d A B C D A B = C D A B C D A = C B = D
15 14 ex A B C D A B = C D A B C D A = C B = D
16 15 pm2.43a A B C D A B = C D A = C B = D
17 16 imp A B C D A B = C D A = C B = D