Metamath Proof Explorer

Theorem mob2

Description: Consequence of "at most one." (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypothesis moi2.1 ⊢ x = A → φ ↔ ψ
Assertion mob2 ⊢ A ∈ B ∧ ∃* x φ ∧ φ → x = A ↔ ψ

Proof

Step Hyp Ref Expression
1 moi2.1 ⊢ x = A → φ ↔ ψ
2 simp3 ⊢ A ∈ B ∧ ∃* x φ ∧ φ → φ
3 2 1 syl5ibcom ⊢ A ∈ B ∧ ∃* x φ ∧ φ → x = A → ψ
4 nfv ⊢ Ⅎ x ψ
5 4 1 sbhypf ⊢ y = A → y x φ ↔ ψ
6 5 anbi2d ⊢ y = A → φ ∧ y x φ ↔ φ ∧ ψ
7 eqeq2 ⊢ y = A → x = y ↔ x = A
8 6 7 imbi12d ⊢ y = A → φ ∧ y x φ → x = y ↔ φ ∧ ψ → x = A
9 8 spcgv ⊢ A ∈ B → ∀ y φ ∧ y x φ → x = y → φ ∧ ψ → x = A
10 nfs1v ⊢ Ⅎ x y x φ
11 sbequ12 ⊢ x = y → φ ↔ y x φ
12 10 11 mo4f ⊢ ∃* x φ ↔ ∀ x ∀ y φ ∧ y x φ → x = y
13 sp ⊢ ∀ x ∀ y φ ∧ y x φ → x = y → ∀ y φ ∧ y x φ → x = y
14 12 13 sylbi ⊢ ∃* x φ → ∀ y φ ∧ y x φ → x = y
15 9 14 impel ⊢ A ∈ B ∧ ∃* x φ → φ ∧ ψ → x = A
16 15 expd ⊢ A ∈ B ∧ ∃* x φ → φ → ψ → x = A
17 16 3impia ⊢ A ∈ B ∧ ∃* x φ ∧ φ → ψ → x = A
18 3 17 impbid ⊢ A ∈ B ∧ ∃* x φ ∧ φ → x = A ↔ ψ