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 elex ⊢ A ∈ V → A ∈ V
9 8 adantr ⊢ A ∈ V ∧ B ∈ W → A ∈ V
10 elex ⊢ B ∈ W → B ∈ V
11 10 adantl ⊢ A ∈ V ∧ B ∈ W → B ∈ V
12 9 11 preqsnd ⊢ A ∈ V ∧ B ∈ W → A B = A ↔ A = A ∧ B = A
13 simpr ⊢ A = A ∧ B = A → B = A
14 eqid ⊢ A = A
15 14 jctl ⊢ B = A → A = A ∧ B = A
16 13 15 impbii ⊢ A = A ∧ B = A ↔ B = A
17 eqcom ⊢ B = A ↔ A = B
18 16 17 bitri ⊢ A = A ∧ B = A ↔ A = B
19 12 18 syl6bb ⊢ A ∈ V ∧ B ∈ W → A B = A ↔ A = B
20 7 19 syl5bb ⊢ A ∈ V ∧ B ∈ W → A = A B ↔ A = B
21 20 anbi1d ⊢ A ∈ V ∧ B ∈ W → A = A B ∧ A B = C ↔ A = B ∧ A B = C
22 dfsn2 ⊢ A = A A
23 preq2 ⊢ A = B → A A = A B
24 22 23 syl5req ⊢ A = B → A B = A
25 24 eqeq1d ⊢ A = B → A B = C ↔ A = C
26 eqcom ⊢ A = C ↔ C = A
27 25 26 syl6bb ⊢ A = B → A B = C ↔ C = A
28 27 a1i ⊢ A ∈ V ∧ B ∈ W → A = B → A B = C ↔ C = A
29 28 pm5.32d ⊢ A ∈ V ∧ B ∈ W → A = B ∧ A B = C ↔ A = B ∧ C = A
30 21 29 bitrd ⊢ A ∈ V ∧ B ∈ W → A = A B ∧ A B = C ↔ A = B ∧ C = A
31 2 6 30 3bitrd ⊢ A ∈ V ∧ B ∈ W → A B = C ↔ A = B ∧ C = A