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