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

Metamath Proof Explorer

Theorem reusv1

Description: Two ways to express single-valuedness of a class expression C ( y ) . (Contributed by NM, 16-Dec-2012) (Proof shortened by Mario Carneiro, 18-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

Ref Expression
Assertion reusv1 ⊢ ∃ y ∈ B φ → ∃! x ∈ A ∀ y ∈ B φ → x = C ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ y ∀ y ∈ B φ → x = C
2 1 nfmov ⊢ Ⅎ y ∃* x ∀ y ∈ B φ → x = C
3 rsp ⊢ ∀ y ∈ B φ → x = C → y ∈ B → φ → x = C
4 3 com3l ⊢ y ∈ B → φ → ∀ y ∈ B φ → x = C → x = C
5 4 alrimdv ⊢ y ∈ B → φ → ∀ x ∀ y ∈ B φ → x = C → x = C
6 mo2icl ⊢ ∀ x ∀ y ∈ B φ → x = C → x = C → ∃* x ∀ y ∈ B φ → x = C
7 5 6 syl6 ⊢ y ∈ B → φ → ∃* x ∀ y ∈ B φ → x = C
8 2 7 rexlimi ⊢ ∃ y ∈ B φ → ∃* x ∀ y ∈ B φ → x = C
9 mormo ⊢ ∃* x ∀ y ∈ B φ → x = C → ∃* x ∈ A ∀ y ∈ B φ → x = C
10 reu5 ⊢ ∃! x ∈ A ∀ y ∈ B φ → x = C ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C ∧ ∃* x ∈ A ∀ y ∈ B φ → x = C
11 10 rbaib ⊢ ∃* x ∈ A ∀ y ∈ B φ → x = C → ∃! x ∈ A ∀ y ∈ B φ → x = C ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C
12 8 9 11 3syl ⊢ ∃ y ∈ B φ → ∃! x ∈ A ∀ y ∈ B φ → x = C ↔ ∃ x ∈ A ∀ y ∈ B φ → x = C