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

Metamath Proof Explorer

Theorem eusvobj1

Description: Specify the same object in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Hypothesis eusvobj1.1 ⊢ B ∈ V
Assertion eusvobj1 ⊢ ∃! x ∃ y ∈ A x = B → ι x | ∃ y ∈ A x = B = ι x | ∀ y ∈ A x = B

Proof

Step Hyp Ref Expression
1 eusvobj1.1 ⊢ B ∈ V
2 nfeu1 ⊢ Ⅎ x ∃! x ∃ y ∈ A x = B
3 1 eusvobj2 ⊢ ∃! x ∃ y ∈ A x = B → ∃ y ∈ A x = B ↔ ∀ y ∈ A x = B
4 2 3 alrimi ⊢ ∃! x ∃ y ∈ A x = B → ∀ x ∃ y ∈ A x = B ↔ ∀ y ∈ A x = B
5 iotabi ⊢ ∀ x ∃ y ∈ A x = B ↔ ∀ y ∈ A x = B → ι x | ∃ y ∈ A x = B = ι x | ∀ y ∈ A x = B
6 4 5 syl ⊢ ∃! x ∃ y ∈ A x = B → ι x | ∃ y ∈ A x = B = ι x | ∀ y ∈ A x = B