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

Metamath Proof Explorer

Theorem preleqALT

Description: Alternate proof of preleq , not based on preleqg : Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses preleq.b 
|- B e. _V
preleqALT.d 
|- D e. _V
Assertion preleqALT 
|- ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 preleq.b 
 |-  B e. _V
2 preleqALT.d 
 |-  D e. _V
3 1 jctr 
 |-  ( A e. B -> ( A e. B /\ B e. _V ) )
4 2 jctr 
 |-  ( C e. D -> ( C e. D /\ D e. _V ) )
5 preq12bg 
 |-  ( ( ( A e. B /\ B e. _V ) /\ ( C e. D /\ D e. _V ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
6 3 4 5 syl2an 
 |-  ( ( A e. B /\ C e. D ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
7 6 biimpa 
 |-  ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
8 7 ord 
 |-  ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( -. ( A = C /\ B = D ) -> ( A = D /\ B = C ) ) )
9 en2lp 
 |-  -. ( D e. C /\ C e. D )
10 eleq12 
 |-  ( ( A = D /\ B = C ) -> ( A e. B <-> D e. C ) )
11 10 anbi1d 
 |-  ( ( A = D /\ B = C ) -> ( ( A e. B /\ C e. D ) <-> ( D e. C /\ C e. D ) ) )
12 9 11 mtbiri 
 |-  ( ( A = D /\ B = C ) -> -. ( A e. B /\ C e. D ) )
13 8 12 syl6 
 |-  ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( -. ( A = C /\ B = D ) -> -. ( A e. B /\ C e. D ) ) )
14 13 con4d 
 |-  ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( ( A e. B /\ C e. D ) -> ( A = C /\ B = D ) ) )
15 14 ex 
 |-  ( ( A e. B /\ C e. D ) -> ( { A , B } = { C , D } -> ( ( A e. B /\ C e. D ) -> ( A = C /\ B = D ) ) ) )
16 15 pm2.43a 
 |-  ( ( A e. B /\ C e. D ) -> ( { A , B } = { C , D } -> ( A = C /\ B = D ) ) )
17 16 imp 
 |-  ( ( ( A e. B /\ C e. D ) /\ { A , B } = { C , D } ) -> ( A = C /\ B = D ) )