This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } <-> { A , B } = { C , D } ) )

Proof

Step Hyp Ref Expression
1 ssprss 
 |-  ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
2 1 3adant3 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { 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 e. V /\ B e. W /\ A =/= B ) -> ( ( A = C /\ B = C ) -> { A , B } = { C , D } ) )
7 6 com12 
 |-  ( ( A = C /\ B = C ) -> ( ( A e. V /\ B e. 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 e. V /\ B e. 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 e. V /\ B e. 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 e. V /\ B e. W /\ A =/= B ) -> ( ( A = D /\ B = D ) -> { A , B } = { C , D } ) )
17 16 com12 
 |-  ( ( A = D /\ B = D ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } = { C , D } ) )
18 7 11 13 17 ccase 
 |-  ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } = { C , D } ) )
19 18 com12 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> { A , B } = { C , D } ) )
20 2 19 sylbid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } -> { A , B } = { C , D } ) )
21 eqimss 
 |-  ( { A , B } = { C , D } -> { A , B } C_ { C , D } )
22 20 21 impbid1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } <-> { A , B } = { C , D } ) )