Metamath Proof Explorer

Theorem rmo4f

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by Thierry Arnoux, 11-Oct-2016) (Revised by Thierry Arnoux, 8-Mar-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo4f.1 ⊢ Ⅎ _ x A
rmo4f.2 ⊢ Ⅎ _ y A
rmo4f.3 ⊢ Ⅎ x ψ
rmo4f.4 ⊢ x = y → φ ↔ ψ
Assertion rmo4f ⊢ ∃* x ∈ A φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ → x = y

Proof

Step Hyp Ref Expression
1 rmo4f.1 ⊢ Ⅎ _ x A
2 rmo4f.2 ⊢ Ⅎ _ y A
3 rmo4f.3 ⊢ Ⅎ x ψ
4 rmo4f.4 ⊢ x = y → φ ↔ ψ
5 nfv ⊢ Ⅎ y φ
6 1 2 5 rmo3f ⊢ ∃* x ∈ A φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ y x φ → x = y
7 3 4 sbiev ⊢ y x φ ↔ ψ
8 7 anbi2i ⊢ φ ∧ y x φ ↔ φ ∧ ψ
9 8 imbi1i ⊢ φ ∧ y x φ → x = y ↔ φ ∧ ψ → x = y
10 9 2ralbii ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ y x φ → x = y ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ → x = y
11 6 10 bitri ⊢ ∃* x ∈ A φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ → x = y