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 ) )