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 ⊢ A ∈ V ∧ B ∈ W → A B = C ↔ A = B ∧ C = A

Proof

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