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	⊢ 𝐴 ∈ V
		funsndifnop.b	⊢ 𝐵 ∈ V
		funsndifnop.g	⊢ 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ }
	Assertion	funsneqopb	⊢ ( 𝐴 = 𝐵 ↔ 𝐺 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		funsndifnop.a	⊢ 𝐴 ∈ V
2		funsndifnop.b	⊢ 𝐵 ∈ V
3		funsndifnop.g	⊢ 𝐺 = { ⟨ 𝐴 , 𝐵 ⟩ }
4		opeq1	⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐵 , 𝐵 ⟩ )
5	4	sneqd	⊢ ( 𝐴 = 𝐵 → { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐵 ⟩ } )
6	2	snopeqopsnid	⊢ { ⟨ 𝐵 , 𝐵 ⟩ } = ⟨ { 𝐵 } , { 𝐵 } ⟩
7	5 6	eqtrdi	⊢ ( 𝐴 = 𝐵 → { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ { 𝐵 } , { 𝐵 } ⟩ )
8	3 7	eqtrid	⊢ ( 𝐴 = 𝐵 → 𝐺 = ⟨ { 𝐵 } , { 𝐵 } ⟩ )
9		snex	⊢ { 𝐵 } ∈ V
10	9 9	opelvv	⊢ ⟨ { 𝐵 } , { 𝐵 } ⟩ ∈ ( V × V )
11	8 10	eqeltrdi	⊢ ( 𝐴 = 𝐵 → 𝐺 ∈ ( V × V ) )
12	1 2 3	funsndifnop	⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐺 ∈ ( V × V ) )
13	12	necon4ai	⊢ ( 𝐺 ∈ ( V × V ) → 𝐴 = 𝐵 )
14	11 13	impbii	⊢ ( 𝐴 = 𝐵 ↔ 𝐺 ∈ ( V × V ) )