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