Theorem preq12b

Description: Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996)

	Ref	Expression
Hypotheses	preqr1.a	$$⊢A\in \mathrm{V}$$
	preqr1.b	$$⊢B\in \mathrm{V}$$
	preq12b.c	$$⊢C\in \mathrm{V}$$
	preq12b.d	$$⊢D\in \mathrm{V}$$
Assertion	preq12b	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\leftrightarrow \left(\left(A=C\wedge B=D\right)\vee \left(A=D\wedge B=C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	$$⊢A\in \mathrm{V}$$
2		preqr1.b	$$⊢B\in \mathrm{V}$$
3		preq12b.c	$$⊢C\in \mathrm{V}$$
4		preq12b.d	$$⊢D\in \mathrm{V}$$
5	1	prid1	$$⊢A\in \left\{A,B\right\}$$
6		eleq2	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A\in \left\{A,B\right\}\leftrightarrow A\in \left\{C,D\right\}\right)$$
7	5 6	mpbii	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to A\in \left\{C,D\right\}$$
8	1	elpr	$$⊢A\in \left\{C,D\right\}\leftrightarrow \left(A=C\vee A=D\right)$$
9	7 8	sylib	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A=C\vee A=D\right)$$
10		preq1	$$⊢A=C\to \left\{A,B\right\}=\left\{C,B\right\}$$
11	10	eqeq1d	$$⊢A=C\to \left(\left\{A,B\right\}=\left\{C,D\right\}\leftrightarrow \left\{C,B\right\}=\left\{C,D\right\}\right)$$
12	2 4	preqr2	$$⊢\left\{C,B\right\}=\left\{C,D\right\}\to B=D$$
13	11 12	syl6bi	$$⊢A=C\to \left(\left\{A,B\right\}=\left\{C,D\right\}\to B=D\right)$$
14	13	com12	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A=C\to B=D\right)$$
15	14	ancld	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A=C\to \left(A=C\wedge B=D\right)\right)$$
16		prcom	$$⊢\left\{C,D\right\}=\left\{D,C\right\}$$
17	16	eqeq2i	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\leftrightarrow \left\{A,B\right\}=\left\{D,C\right\}$$
18		preq1	$$⊢A=D\to \left\{A,B\right\}=\left\{D,B\right\}$$
19	18	eqeq1d	$$⊢A=D\to \left(\left\{A,B\right\}=\left\{D,C\right\}\leftrightarrow \left\{D,B\right\}=\left\{D,C\right\}\right)$$
20	2 3	preqr2	$$⊢\left\{D,B\right\}=\left\{D,C\right\}\to B=C$$
21	19 20	syl6bi	$$⊢A=D\to \left(\left\{A,B\right\}=\left\{D,C\right\}\to B=C\right)$$
22	21	com12	$$⊢\left\{A,B\right\}=\left\{D,C\right\}\to \left(A=D\to B=C\right)$$
23	17 22	sylbi	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A=D\to B=C\right)$$
24	23	ancld	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(A=D\to \left(A=D\wedge B=C\right)\right)$$
25	15 24	orim12d	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(\left(A=C\vee A=D\right)\to \left(\left(A=C\wedge B=D\right)\vee \left(A=D\wedge B=C\right)\right)\right)$$
26	9 25	mpd	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\to \left(\left(A=C\wedge B=D\right)\vee \left(A=D\wedge B=C\right)\right)$$
27		preq12	$$⊢\left(A=C\wedge B=D\right)\to \left\{A,B\right\}=\left\{C,D\right\}$$
28		preq12	$$⊢\left(A=D\wedge B=C\right)\to \left\{A,B\right\}=\left\{D,C\right\}$$
29		prcom	$$⊢\left\{D,C\right\}=\left\{C,D\right\}$$
30	28 29	eqtrdi	$$⊢\left(A=D\wedge B=C\right)\to \left\{A,B\right\}=\left\{C,D\right\}$$
31	27 30	jaoi	$$⊢\left(\left(A=C\wedge B=D\right)\vee \left(A=D\wedge B=C\right)\right)\to \left\{A,B\right\}=\left\{C,D\right\}$$
32	26 31	impbii	$$⊢\left\{A,B\right\}=\left\{C,D\right\}\leftrightarrow \left(\left(A=C\wedge B=D\right)\vee \left(A=D\wedge B=C\right)\right)$$