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

Proof

Step	Hyp	Ref	Expression
1		bm1.3ii.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	⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝜑 )