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 ⊢ ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑥 )
Assertion bm1.3iiOLD ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 )

Proof

Step Hyp Ref Expression
1 bm1.3iiOLD.1 ⊢ ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑥 )
2 19.42v ⊢ ( ∃ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) ↔ ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) )
3 bimsc1 ⊢ ( ( ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) → ( 𝑦 ∈ 𝑥 ↔ 𝜑 ) )
4 3 alanimi ⊢ ( ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) → ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 ) )
5 4 eximi ⊢ ( ∃ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 ) )
6 2 5 sylbir ⊢ ( ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) ) → ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 ) )
7 elequ2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 → 𝑦 ∈ 𝑥 ) ↔ ( 𝜑 → 𝑦 ∈ 𝑧 ) ) )
9 8 albidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ) )
10 9 cbvexvw ⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) )
11 1 10 mpbi ⊢ ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 )
12 ax-sep ⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) )
13 11 12 exan ⊢ ∃ 𝑧 ( ∀ 𝑦 ( 𝜑 → 𝑦 ∈ 𝑧 ) ∧ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑧 ∧ 𝜑 ) ) )
14 6 13 exlimiiv ⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 )