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

Metamath Proof Explorer

Theorem hash1elsn

Description: A set of size 1 with a known element is the singleton of that element. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses hash1elsn.1 ⊢ φ → A = 1
hash1elsn.2 ⊢ φ → B ∈ A
hash1elsn.3 ⊢ φ → A ∈ V
Assertion hash1elsn ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 hash1elsn.1 ⊢ φ → A = 1
2 hash1elsn.2 ⊢ φ → B ∈ A
3 hash1elsn.3 ⊢ φ → A ∈ V
4 hashen1 ⊢ A ∈ V → A = 1 ↔ A ≈ 1 𝑜
5 3 4 syl ⊢ φ → A = 1 ↔ A ≈ 1 𝑜
6 1 5 mpbid ⊢ φ → A ≈ 1 𝑜
7 en1 ⊢ A ≈ 1 𝑜 ↔ ∃ x A = x
8 6 7 sylib ⊢ φ → ∃ x A = x
9 simpr ⊢ φ ∧ A = x → A = x
10 2 adantr ⊢ φ ∧ A = x → B ∈ A
11 10 9 eleqtrd ⊢ φ ∧ A = x → B ∈ x
12 elsni ⊢ B ∈ x → B = x
13 11 12 syl ⊢ φ ∧ A = x → B = x
14 13 sneqd ⊢ φ ∧ A = x → B = x
15 9 14 eqtr4d ⊢ φ ∧ A = x → A = B
16 8 15 exlimddv ⊢ φ → A = B