Theorem opprb

Description: Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023)

	Ref	Expression
Assertion	opprb	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐶 ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		preq12bg	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
2		opthg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
3	2	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
4		opthg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐶 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐶 ⟩ ↔ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
6	3 5	orbi12d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐶 ⟩ ) ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )
7	1 6	bitr4d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐷 , 𝐶 ⟩ ) ) )