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→AB⊆CD↔AB=CD

Proof

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