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→AB=C↔A=B∧C=A

Proof

Step Hyp Ref Expression
1 dfopg ⊢A∈V∧B∈W→AB=AAB
2 1 eqeq1d ⊢A∈V∧B∈W→AB=C↔AAB=C
3 snex ⊢A∈V
4 prex ⊢AB∈V
5 3 4 preqsn ⊢AAB=C↔A=AB∧AB=C
6 5 a1i ⊢A∈V∧B∈W→AAB=C↔A=AB∧AB=C
7 eqcom ⊢A=AB↔AB=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→AB=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→AB=A↔A=B
18 7 17 bitrid ⊢A∈V∧B∈W→A=AB↔A=B
19 18 anbi1d ⊢A∈V∧B∈W→A=AB∧AB=C↔A=B∧AB=C
20 dfsn2 ⊢A=AA
21 preq2 ⊢A=B→AA=AB
22 20 21 eqtr2id ⊢A=B→AB=A
23 22 eqeq1d ⊢A=B→AB=C↔A=C
24 eqcom ⊢A=C↔C=A
25 23 24 bitrdi ⊢A=B→AB=C↔C=A
26 25 a1i ⊢A∈V∧B∈W→A=B→AB=C↔C=A
27 26 pm5.32d ⊢A∈V∧B∈W→A=B∧AB=C↔A=B∧C=A
28 19 27 bitrd ⊢A∈V∧B∈W→A=AB∧AB=C↔A=B∧C=A
29 2 6 28 3bitrd ⊢A∈V∧B∈W→AB=C↔A=B∧C=A