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

Metamath Proof Explorer

Theorem ssprsseq

Description: A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion ssprsseq ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )

Proof

Step Hyp Ref Expression
1 ssprss ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )
3 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
4 eqtr3 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
5 3 4 syl11 ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
6 5 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
7 6 com12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
8 preq12 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐷 , 𝐶 } )
9 prcom ⊢ { 𝐷 , 𝐶 } = { 𝐶 , 𝐷 }
10 8 9 eqtrdi ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
11 10 a1d ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
12 preq12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
13 12 a1d ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
14 eqtr3 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → 𝐴 = 𝐵 )
15 3 14 syl11 ⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
17 16 com12 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
18 7 11 13 17 ccase ⊢ ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
19 18 com12 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
20 2 19 sylbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )
21 eqimss ⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } )
22 20 21 impbid1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )