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∀yy∈x↔φ

Proof

Step Hyp Ref Expression
1 bm1.3ii.1 ⊢∃x∀yφ→y∈x
2 19.42v ⊢∃x∀yφ→y∈z∧∀yy∈x↔y∈z∧φ↔∀yφ→y∈z∧∃x∀yy∈x↔y∈z∧φ
3 bimsc1 ⊢φ→y∈z∧y∈x↔y∈z∧φ→y∈x↔φ
4 3 alanimi ⊢∀yφ→y∈z∧∀yy∈x↔y∈z∧φ→∀yy∈x↔φ
5 4 eximi ⊢∃x∀yφ→y∈z∧∀yy∈x↔y∈z∧φ→∃x∀yy∈x↔φ
6 2 5 sylbir ⊢∀yφ→y∈z∧∃x∀yy∈x↔y∈z∧φ→∃x∀yy∈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∀yy∈x↔y∈z∧φ
13 11 12 exan ⊢∃z∀yφ→y∈z∧∃x∀yy∈x↔y∈z∧φ
14 6 13 exlimiiv ⊢∃x∀yy∈x↔φ