# Metamath Proof Explorer

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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}↔\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 ssprss ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}↔\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)\right)$
2 1 3adant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}↔\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)\right)$
3 eqneqall ${⊢}{A}={B}\to \left({A}\ne {B}\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
4 eqtr3 ${⊢}\left({A}={C}\wedge {B}={C}\right)\to {A}={B}$
5 3 4 syl11 ${⊢}{A}\ne {B}\to \left(\left({A}={C}\wedge {B}={C}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
6 5 3ad2ant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left({A}={C}\wedge {B}={C}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
7 6 com12 ${⊢}\left({A}={C}\wedge {B}={C}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
8 preq12 ${⊢}\left({A}={D}\wedge {B}={C}\right)\to \left\{{A},{B}\right\}=\left\{{D},{C}\right\}$
9 prcom ${⊢}\left\{{D},{C}\right\}=\left\{{C},{D}\right\}$
10 8 9 eqtrdi ${⊢}\left({A}={D}\wedge {B}={C}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}$
11 10 a1d ${⊢}\left({A}={D}\wedge {B}={C}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
12 preq12 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}$
13 12 a1d ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
14 eqtr3 ${⊢}\left({A}={D}\wedge {B}={D}\right)\to {A}={B}$
15 3 14 syl11 ${⊢}{A}\ne {B}\to \left(\left({A}={D}\wedge {B}={D}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
16 15 3ad2ant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left({A}={D}\wedge {B}={D}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
17 16 com12 ${⊢}\left({A}={D}\wedge {B}={D}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
18 7 11 13 17 ccase ${⊢}\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
19 18 com12 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
20 2 19 sylbid ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$
21 eqimss ${⊢}\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}$
22 20 21 impbid1 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}\subseteq \left\{{C},{D}\right\}↔\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\right)$