Metamath Proof Explorer

Theorem ssprsseq

Description: A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion ssprsseq ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ⊆ C D ↔ A B = C D

Proof

Step Hyp Ref Expression
1 ssprss ⊢ A ∈ V ∧ B ∈ W → A B ⊆ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D
2 1 3adant3 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ⊆ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D
3 eqneqall ⊢ A = B → A ≠ B → A B = C D
4 eqtr3 ⊢ A = C ∧ B = C → A = B
5 3 4 syl11 ⊢ A ≠ B → A = C ∧ B = C → A B = C D
6 5 3ad2ant3 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∧ B = C → A B = C D
7 6 com12 ⊢ A = C ∧ B = C → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D
8 preq12 ⊢ A = D ∧ B = C → A B = D C
9 prcom ⊢ D C = C D
10 8 9 eqtrdi ⊢ A = D ∧ B = C → A B = C D
11 10 a1d ⊢ A = D ∧ B = C → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D
12 preq12 ⊢ A = C ∧ B = D → A B = C D
13 12 a1d ⊢ A = C ∧ B = D → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D
14 eqtr3 ⊢ A = D ∧ B = D → A = B
15 3 14 syl11 ⊢ A ≠ B → A = D ∧ B = D → A B = C D
16 15 3ad2ant3 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = D ∧ B = D → A B = C D
17 16 com12 ⊢ A = D ∧ B = D → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D
18 7 11 13 17 ccase ⊢ A = C ∨ A = D ∧ B = C ∨ B = D → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D
19 18 com12 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∨ A = D ∧ B = C ∨ B = D → A B = C D
20 2 19 sylbid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ⊆ C D → A B = C D
21 eqimss ⊢ A B = C D → A B ⊆ C D
22 20 21 impbid1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ⊆ C D ↔ A B = C D