Theorem bm1.3ii 2702

Description: Convert implication to equivalence using Aussonderung. Similar to Theorem 1.3ii of [BellMachover] p. 463.

Hypothesis

Ref	Expression
bm1.3ii.1	⊢ ∃x∀y(φ → y ∈ x)

Assertion

Ref	Expression
bm1.3ii	⊢ ∃x∀y(y ∈ x ↔ φ)

Distinct variable groups:   φ,x   x,y

Proof of Theorem bm1.3ii

Step	Hyp	Ref	Expression
1		bm1.3ii.1	. . . . 5 ⊢ ∃x∀y(φ → y ∈ x)
2		elequ2 1135	. . . . . . . 8 ⊢ (x = z → (y ∈ x ↔ y ∈ z))
3	2	imbi2d 611	. . . . . . 7 ⊢ (x = z → ((φ → y ∈ x) ↔ (φ → y ∈ z)))
4	3	albidv 1276	. . . . . 6 ⊢ (x = z → (∀y(φ → y ∈ x) ↔ ∀y(φ → y ∈ z)))
5	4	cbvexv 1313	. . . . 5 ⊢ (∃x∀y(φ → y ∈ x) ↔ ∃z∀y(φ → y ∈ z))
6	1, 5	mpbi 189	. . . 4 ⊢ ∃z∀y(φ → y ∈ z)
7		ax-sep 2699	. . . 4 ⊢ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ))
8	6, 7	pm3.2i 285	. . 3 ⊢ (∃z∀y(φ → y ∈ z) ⋀ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ)))
9	8	exan 1104	. 2 ⊢ ∃z(∀y(φ → y ∈ z) ⋀ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ)))
10		19.42v 1306	. . . 4 ⊢ (∃x(∀y(φ → y ∈ z) ⋀ ∀y(y ∈ x ↔ (y ∈ z ⋀ φ))) ↔ (∀y(φ → y ∈ z) ⋀ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ))))
11		19.26 1065	. . . . . 6 ⊢ (∀y((φ → y ∈ z) ⋀ (y ∈ x ↔ (y ∈ z ⋀ φ))) ↔ (∀y(φ → y ∈ z) ⋀ ∀y(y ∈ x ↔ (y ∈ z ⋀ φ))))
12		bimsc1 749	. . . . . . 7 ⊢ (((φ → y ∈ z) ⋀ (y ∈ x ↔ (y ∈ z ⋀ φ))) → (y ∈ x ↔ φ))
13	12	19.20i 990	. . . . . 6 ⊢ (∀y((φ → y ∈ z) ⋀ (y ∈ x ↔ (y ∈ z ⋀ φ))) → ∀y(y ∈ x ↔ φ))
14	11, 13	sylbir 201	. . . . 5 ⊢ ((∀y(φ → y ∈ z) ⋀ ∀y(y ∈ x ↔ (y ∈ z ⋀ φ))) → ∀y(y ∈ x ↔ φ))
15	14	19.22i 1038	. . . 4 ⊢ (∃x(∀y(φ → y ∈ z) ⋀ ∀y(y ∈ x ↔ (y ∈ z ⋀ φ))) → ∃x∀y(y ∈ x ↔ φ))
16	10, 15	sylbir 201	. . 3 ⊢ ((∀y(φ → y ∈ z) ⋀ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ))) → ∃x∀y(y ∈ x ↔ φ))
17	16	19.23aiv 1293	. 2 ⊢ (∃z(∀y(φ → y ∈ z) ⋀ ∃x∀y(y ∈ x ↔ (y ∈ z ⋀ φ))) → ∃x∀y(y ∈ x ↔ φ))
18	9, 17	ax-mp 7	1 ⊢ ∃x∀y(y ∈ x ↔ φ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978

This theorem is referenced by:  axpow2 2740  pwex 2741  zfpair2 2776  axun2 2867  uniex2 2868

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-sep 2699

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979

Copyright terms: Public domain