Metamath Proof Explorer

Theorem opeqsn

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
Hypotheses opeqsn.1 ⊢ A ∈ V
opeqsn.2 ⊢ B ∈ V
Assertion opeqsn ⊢ A B = C ↔ A = B ∧ C = A

Proof

Step Hyp Ref Expression
1 opeqsn.1 ⊢ A ∈ V
2 opeqsn.2 ⊢ B ∈ V
3 opeqsng ⊢ A ∈ V ∧ B ∈ V → A B = C ↔ A = B ∧ C = A
4 1 2 3 mp2an ⊢ A B = C ↔ A = B ∧ C = A