Metamath Proof Explorer

Theorem opeqsng

Description: Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

Ref Expression
Assertion opeqsng ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 dfopg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ↔ { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝐶 } ) )
3 snex ⊢ { 𝐴 } ∈ V
4 prex ⊢ { 𝐴 , 𝐵 } ∈ V
5 3 4 preqsn ⊢ ( { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝐶 } ↔ ( { 𝐴 } = { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } = 𝐶 ) )
6 5 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝐶 } ↔ ( { 𝐴 } = { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } = 𝐶 ) ) )
7 eqcom ⊢ ( { 𝐴 } = { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } = { 𝐴 } )
8 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
9 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
10 8 9 preqsnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 , 𝐵 } = { 𝐴 } ↔ ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐴 ) ) )
11 simpr ⊢ ( ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐴 ) → 𝐵 = 𝐴 )
12 eqid ⊢ 𝐴 = 𝐴
13 12 jctl ⊢ ( 𝐵 = 𝐴 → ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐴 ) )
14 11 13 impbii ⊢ ( ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐴 ) ↔ 𝐵 = 𝐴 )
15 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
16 14 15 bitri ⊢ ( ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐴 ) ↔ 𝐴 = 𝐵 )
17 10 16 bitrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 , 𝐵 } = { 𝐴 } ↔ 𝐴 = 𝐵 ) )
18 7 17 syl5bb ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } = { 𝐴 , 𝐵 } ↔ 𝐴 = 𝐵 ) )
19 18 anbi1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } = { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ { 𝐴 , 𝐵 } = 𝐶 ) ) )
20 dfsn2 ⊢ { 𝐴 } = { 𝐴 , 𝐴 }
21 preq2 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
22 20 21 eqtr2id ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
23 22 eqeq1d ⊢ ( 𝐴 = 𝐵 → ( { 𝐴 , 𝐵 } = 𝐶 ↔ { 𝐴 } = 𝐶 ) )
24 eqcom ⊢ ( { 𝐴 } = 𝐶 ↔ 𝐶 = { 𝐴 } )
25 23 24 bitrdi ⊢ ( 𝐴 = 𝐵 → ( { 𝐴 , 𝐵 } = 𝐶 ↔ 𝐶 = { 𝐴 } ) )
26 25 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 = 𝐵 → ( { 𝐴 , 𝐵 } = 𝐶 ↔ 𝐶 = { 𝐴 } ) ) )
27 26 pm5.32d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 = 𝐵 ∧ { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )
28 19 27 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } = { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } = 𝐶 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )
29 2 6 28 3bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = { 𝐶 } ↔ ( 𝐴 = 𝐵 ∧ 𝐶 = { 𝐴 } ) ) )