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

Metamath Proof Explorer

Theorem bm1.3iiOLD

Description: Obsolete version of sepexi as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bm1.3iiOLD.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 ↔ φ