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	⊢ 𝐵 ∈ V
Assertion	preleq	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		preleq.b	⊢ 𝐵 ∈ V
2		preleqg	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
3	1 2	mp3anl2	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )