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

Metamath Proof Explorer

Theorem preq12nebg

Description: Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022)

Ref Expression
Assertion preq12nebg 
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )

Proof

Step Hyp Ref Expression
1 3simpa 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A e. V /\ B e. W ) )
2 1 anim1i 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ ( C e. _V /\ D e. _V ) ) -> ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ D e. _V ) ) )
3 2 ancoms 
 |-  ( ( ( C e. _V /\ D e. _V ) /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ D e. _V ) ) )
4 preq12bg 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. _V /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
5 3 4 syl 
 |-  ( ( ( C e. _V /\ D e. _V ) /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
6 5 ex 
 |-  ( ( C e. _V /\ D e. _V ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) ) )
7 ianor 
 |-  ( -. ( C e. _V /\ D e. _V ) <-> ( -. C e. _V \/ -. D e. _V ) )
8 prneprprc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. C e. _V ) -> { A , B } =/= { C , D } )
9 8 ancoms 
 |-  ( ( -. C e. _V /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> { A , B } =/= { C , D } )
10 eqneqall 
 |-  ( { A , B } = { C , D } -> ( { A , B } =/= { C , D } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
11 9 10 syl5com 
 |-  ( ( -. C e. _V /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( { A , B } = { C , D } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
12 prneprprc 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ -. D e. _V ) -> { A , B } =/= { D , C } )
13 12 ancoms 
 |-  ( ( -. D e. _V /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> { A , B } =/= { D , C } )
14 prcom 
 |-  { C , D } = { D , C }
15 14 eqeq2i 
 |-  ( { A , B } = { C , D } <-> { A , B } = { D , C } )
16 eqneqall 
 |-  ( { A , B } = { D , C } -> ( { A , B } =/= { D , C } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
17 15 16 sylbi 
 |-  ( { A , B } = { C , D } -> ( { A , B } =/= { D , C } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
18 13 17 syl5com 
 |-  ( ( -. D e. _V /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( { A , B } = { C , D } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
19 11 18 jaoian 
 |-  ( ( ( -. C e. _V \/ -. D e. _V ) /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( { A , B } = { C , D } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
20 preq12 
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
21 preq12 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { D , C } )
22 prcom 
 |-  { D , C } = { C , D }
23 21 22 eqtrdi 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { C , D } )
24 20 23 jaoi 
 |-  ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> { A , B } = { C , D } )
25 19 24 impbid1 
 |-  ( ( ( -. C e. _V \/ -. D e. _V ) /\ ( A e. V /\ B e. W /\ A =/= B ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
26 25 ex 
 |-  ( ( -. C e. _V \/ -. D e. _V ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) ) )
27 7 26 sylbi 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) ) )
28 6 27 pm2.61i 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )