Metamath Proof Explorer

Theorem bm1.3ii

Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis bm1.3ii.1 ⊢ ∃ x ∀ y φ → y ∈ x
Assertion bm1.3ii ⊢ ∃ x ∀ y y ∈ x ↔ φ

Proof

Step Hyp Ref Expression
1 bm1.3ii.1 ⊢ ∃ x ∀ y φ → y ∈ x
2 19.42v ⊢ ∃ x ∀ y φ → y ∈ z ∧ ∀ y y ∈ x ↔ y ∈ z ∧ φ ↔ ∀ y φ → y ∈ z ∧ ∃ x ∀ y y ∈ x ↔ y ∈ z ∧ φ
3 bimsc1 ⊢ φ → y ∈ z ∧ y ∈ x ↔ y ∈ z ∧ φ → y ∈ x ↔ φ
4 3 alanimi ⊢ ∀ y φ → y ∈ z ∧ ∀ y y ∈ x ↔ y ∈ z ∧ φ → ∀ y y ∈ x ↔ φ
5 4 eximi ⊢ ∃ x ∀ y φ → y ∈ z ∧ ∀ y y ∈ x ↔ y ∈ z ∧ φ → ∃ x ∀ y y ∈ x ↔ φ
6 2 5 sylbir ⊢ ∀ y φ → y ∈ z ∧ ∃ x ∀ y y ∈ x ↔ y ∈ z ∧ φ → ∃ x ∀ y y ∈ x ↔ φ
7 elequ2 ⊢ x = z → y ∈ x ↔ y ∈ z
8 7 imbi2d ⊢ x = z → φ → y ∈ x ↔ φ → y ∈ z
9 8 albidv ⊢ x = z → ∀ y φ → y ∈ x ↔ ∀ y φ → y ∈ z
10 9 cbvexvw ⊢ ∃ x ∀ y φ → y ∈ x ↔ ∃ z ∀ y φ → y ∈ z
11 1 10 mpbi ⊢ ∃ z ∀ y φ → y ∈ z
12 ax-sep ⊢ ∃ x ∀ y y ∈ x ↔ y ∈ z ∧ φ
13 11 12 exan ⊢ ∃ z ∀ y φ → y ∈ z ∧ ∃ x ∀ y y ∈ x ↔ y ∈ z ∧ φ
14 6 13 exlimiiv ⊢ ∃ x ∀ y y ∈ x ↔ φ