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

Metamath Proof Explorer

Theorem prel12g

Description: Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996) (Revised by AV, 9-Dec-2018) (Revised by AV, 12-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 preq12nebg 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
2 prid1g 
 |-  ( A e. V -> A e. { A , D } )
3 2 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> A e. { A , D } )
4 3 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ A = C ) -> A e. { A , D } )
5 preq1 
 |-  ( A = C -> { A , D } = { C , D } )
6 5 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ A = C ) -> { A , D } = { C , D } )
7 4 6 eleqtrd 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ A = C ) -> A e. { C , D } )
8 7 ex 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A = C -> A e. { C , D } ) )
9 prid2g 
 |-  ( B e. W -> B e. { C , B } )
10 9 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> B e. { C , B } )
11 preq2 
 |-  ( B = D -> { C , B } = { C , D } )
12 11 eleq2d 
 |-  ( B = D -> ( B e. { C , B } <-> B e. { C , D } ) )
13 10 12 syl5ibcom 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( B = D -> B e. { C , D } ) )
14 8 13 anim12d 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( A = C /\ B = D ) -> ( A e. { C , D } /\ B e. { C , D } ) ) )
15 prid2g 
 |-  ( A e. V -> A e. { C , A } )
16 15 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> A e. { C , A } )
17 preq2 
 |-  ( A = D -> { C , A } = { C , D } )
18 17 eleq2d 
 |-  ( A = D -> ( A e. { C , A } <-> A e. { C , D } ) )
19 16 18 syl5ibcom 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A = D -> A e. { C , D } ) )
20 prid1g 
 |-  ( B e. W -> B e. { B , D } )
21 20 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> B e. { B , D } )
22 preq1 
 |-  ( B = C -> { B , D } = { C , D } )
23 22 eleq2d 
 |-  ( B = C -> ( B e. { B , D } <-> B e. { C , D } ) )
24 21 23 syl5ibcom 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( B = C -> B e. { C , D } ) )
25 19 24 anim12d 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( A = D /\ B = C ) -> ( A e. { C , D } /\ B e. { C , D } ) ) )
26 14 25 jaod 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( A e. { C , D } /\ B e. { C , D } ) ) )
27 elprg 
 |-  ( A e. V -> ( A e. { C , D } <-> ( A = C \/ A = D ) ) )
28 27 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( A e. { C , D } <-> ( A = C \/ A = D ) ) )
29 elprg 
 |-  ( B e. W -> ( B e. { C , D } <-> ( B = C \/ B = D ) ) )
30 29 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( B e. { C , D } <-> ( B = C \/ B = D ) ) )
31 28 30 anbi12d 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( A e. { C , D } /\ B e. { C , D } ) <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
32 eqtr3 
 |-  ( ( A = C /\ B = C ) -> A = B )
33 eqneqall 
 |-  ( A = B -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
34 32 33 syl 
 |-  ( ( A = C /\ B = C ) -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
35 olc 
 |-  ( ( A = D /\ B = C ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
36 35 a1d 
 |-  ( ( A = D /\ B = C ) -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
37 orc 
 |-  ( ( A = C /\ B = D ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
38 37 a1d 
 |-  ( ( A = C /\ B = D ) -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
39 eqtr3 
 |-  ( ( A = D /\ B = D ) -> A = B )
40 39 33 syl 
 |-  ( ( A = D /\ B = D ) -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
41 34 36 38 40 ccase 
 |-  ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> ( A =/= B -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
42 41 com12 
 |-  ( A =/= B -> ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
43 42 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
44 31 43 sylbid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( A e. { C , D } /\ B e. { C , D } ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
45 26 44 impbid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A e. { C , D } /\ B e. { C , D } ) ) )
46 1 45 bitrd 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( A e. { C , D } /\ B e. { C , D } ) ) )