This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funsneqopb

Description: A singleton of an ordered pair is an ordered pair iff the components are equal. (Contributed by AV, 24-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Hypotheses funsndifnop.a ⊢ A ∈ V
funsndifnop.b ⊢ B ∈ V
funsndifnop.g ⊢ G = A B
Assertion funsneqopb ⊢ A = B ↔ G ∈ V × V

Proof

Step Hyp Ref Expression
1 funsndifnop.a ⊢ A ∈ V
2 funsndifnop.b ⊢ B ∈ V
3 funsndifnop.g ⊢ G = A B
4 opeq1 ⊢ A = B → A B = B B
5 4 sneqd ⊢ A = B → A B = B B
6 2 snopeqopsnid ⊢ B B = B B
7 5 6 eqtrdi ⊢ A = B → A B = B B
8 3 7 eqtrid ⊢ A = B → G = B B
9 snex ⊢ B ∈ V
10 9 9 opelvv ⊢ B B ∈ V × V
11 8 10 eqeltrdi ⊢ A = B → G ∈ V × V
12 1 2 3 funsndifnop ⊢ A ≠ B → ¬ G ∈ V × V
13 12 necon4ai ⊢ G ∈ V × V → A = B
14 11 13 impbii ⊢ A = B ↔ G ∈ V × V