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 ⊢ A B = 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 → A B = C ↔ A = C ∧ B = C
6 1 5 ax-mp ⊢ A B = 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 ⊢ A B = C ↔ A = B ∧ B = C