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

Proof

Step	Hyp	Ref	Expression
1		elneq	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵 )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → 𝐴 ≠ 𝐵 )
3		preq12nebg	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
4	2 3	syld3an3	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
5		eleq12	⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ 𝐷 ∈ 𝐶 ) )
6		elnotel	⊢ ( 𝐷 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐷 )
7	6	pm2.21d	⊢ ( 𝐷 ∈ 𝐶 → ( 𝐶 ∈ 𝐷 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
8	5 7	biimtrdi	⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
9	8	com3l	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
10	9	a1d	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ 𝐷 → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) ) )
11	10	3imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
12	11	com12	⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
13	12	jao1i	⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
14	13	com12	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
15	4 14	sylbid	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
16	15	imp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )