This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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