Metamath Proof Explorer

Theorem preqsn

Description: Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008) (Revised by AV, 12-Jun-2022)

Ref Expression
Hypotheses preqsn.1 ⊢A∈V
preqsn.2 ⊢B∈V
Assertion preqsn ⊢AB=C↔A=B∧B=C

Proof

Step Hyp Ref Expression
1 preqsn.1 ⊢A∈V
2 preqsn.2 ⊢B∈V
3 id ⊢A∈V→A∈V
4 2 a1i ⊢A∈V→B∈V
5 3 4 preqsnd ⊢A∈V→AB=C↔A=C∧B=C
6 1 5 ax-mp ⊢AB=C↔A=C∧B=C
7 eqeq2 ⊢B=C→A=B↔A=C
8 7 pm5.32ri ⊢A=B∧B=C↔A=C∧B=C
9 6 8 bitr4i ⊢AB=C↔A=B∧B=C