Theorem preleq

Description: Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996) (Revised by AV, 15-Jun-2022)

	Ref	Expression
Hypothesis	preleq.b	$$⊢B\in \mathrm{V}$$
Assertion	preleq	$$⊢\left(\left(A\in B\wedge C\in D\right)\wedge \left\{A,B\right\}=\left\{C,D\right\}\right)\to \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		preleq.b	$$⊢B\in \mathrm{V}$$
2		preleqg	$$⊢\left(\left(A\in B\wedge B\in \mathrm{V}\wedge C\in D\right)\wedge \left\{A,B\right\}=\left\{C,D\right\}\right)\to \left(A=C\wedge B=D\right)$$
3	1 2	mp3anl2	$$⊢\left(\left(A\in B\wedge C\in D\right)\wedge \left\{A,B\right\}=\left\{C,D\right\}\right)\to \left(A=C\wedge B=D\right)$$