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

Metamath Proof Explorer

Theorem preleqg

Description: Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq . (Contributed by AV, 15-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 elneq 
 |-  ( A e. B -> A =/= B )
2 1 3ad2ant1 
 |-  ( ( A e. B /\ B e. V /\ C e. D ) -> A =/= B )
3 preq12nebg 
 |-  ( ( A e. B /\ B e. V /\ A =/= B ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
4 2 3 syld3an3 
 |-  ( ( A e. B /\ B e. V /\ C e. D ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
5 eleq12 
 |-  ( ( A = D /\ B = C ) -> ( A e. B <-> D e. C ) )
6 elnotel 
 |-  ( D e. C -> -. C e. D )
7 6 pm2.21d 
 |-  ( D e. C -> ( C e. D -> ( A = C /\ B = D ) ) )
8 5 7 biimtrdi 
 |-  ( ( A = D /\ B = C ) -> ( A e. B -> ( C e. D -> ( A = C /\ B = D ) ) ) )
9 8 com3l 
 |-  ( A e. B -> ( C e. D -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) ) )
10 9 a1d 
 |-  ( A e. B -> ( B e. V -> ( C e. D -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) ) ) )
11 10 3imp 
 |-  ( ( A e. B /\ B e. V /\ C e. D ) -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) )
12 11 com12 
 |-  ( ( A = D /\ B = C ) -> ( ( A e. B /\ B e. V /\ C e. D ) -> ( A = C /\ B = D ) ) )
13 12 jao1i 
 |-  ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( ( A e. B /\ B e. V /\ C e. D ) -> ( A = C /\ B = D ) ) )
14 13 com12 
 |-  ( ( A e. B /\ B e. V /\ C e. D ) -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( A = C /\ B = D ) ) )
15 4 14 sylbid 
 |-  ( ( A e. B /\ B e. V /\ C e. D ) -> ( { A , B } = { C , D } -> ( A = C /\ B = D ) ) )
16 15 imp 
 |-  ( ( ( A e. B /\ B e. V /\ C e. D ) /\ { A , B } = { C , D } ) -> ( A = C /\ B = D ) )