Theorem opeqpr

Description: Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	opeqpr.1	$$⊢A\in \mathrm{V}$$
	opeqpr.2	$$⊢B\in \mathrm{V}$$
	opeqpr.3	$$⊢C\in \mathrm{V}$$
	opeqpr.4	$$⊢D\in \mathrm{V}$$
Assertion	opeqpr	$$⊢⟨A,B⟩=\left\{C,D\right\}\leftrightarrow \left(\left(C=\left\{A\right\}\wedge D=\left\{A,B\right\}\right)\vee \left(C=\left\{A,B\right\}\wedge D=\left\{A\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		opeqpr.1	$$⊢A\in \mathrm{V}$$
2		opeqpr.2	$$⊢B\in \mathrm{V}$$
3		opeqpr.3	$$⊢C\in \mathrm{V}$$
4		opeqpr.4	$$⊢D\in \mathrm{V}$$
5		eqcom	$$⊢⟨A,B⟩=\left\{C,D\right\}\leftrightarrow \left\{C,D\right\}=⟨A,B⟩$$
6	1 2	dfop	$$⊢⟨A,B⟩=\left\{\left\{A\right\},\left\{A,B\right\}\right\}$$
7	6	eqeq2i	$$⊢\left\{C,D\right\}=⟨A,B⟩\leftrightarrow \left\{C,D\right\}=\left\{\left\{A\right\},\left\{A,B\right\}\right\}$$
8		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
9		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
10	3 4 8 9	preq12b	$$⊢\left\{C,D\right\}=\left\{\left\{A\right\},\left\{A,B\right\}\right\}\leftrightarrow \left(\left(C=\left\{A\right\}\wedge D=\left\{A,B\right\}\right)\vee \left(C=\left\{A,B\right\}\wedge D=\left\{A\right\}\right)\right)$$
11	5 7 10	3bitri	$$⊢⟨A,B⟩=\left\{C,D\right\}\leftrightarrow \left(\left(C=\left\{A\right\}\wedge D=\left\{A,B\right\}\right)\vee \left(C=\left\{A,B\right\}\wedge D=\left\{A\right\}\right)\right)$$