Theorem axsep 2692

Description: Separation Scheme, which is an axiom scheme of Zermelo's original theory. Scheme Sep of [BellMachover] p. 463. As we show here, it is redundant if we assume Replacement in the form of ax-rep 2683. Some textbooks present Separation as a separate axiom scheme in order to show that much of set theory can be derived without the stronger Replacement. The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x ∈ z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 1928. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

The variable x can appear free in the wff φ, which in textbooks is often written φ(x). To specify this in the Metamath language, we omit the distinct variable requirement ($d) that x not appear in φ.

For a version using a class variable, see zfauscl 2695, which requires the Axiom of Extensionality as well as Replacement for its derivation.

If we omit the requirement that y not occur in φ, we can derive a contradiction, as notzfaus 2731 shows (contradicting zfauscl 2695). However, as axsep2 2694 shows, we can eliminate the restriction that z not occur in φ.

Note: the distinct variable restriction that z not occur in φ is actually redundant in this particular proof, but we keep it since its purpose is to demonstrate the derivation of the exact ax-sep 2693 from ax-rep 2683.

This theorem should not be referenced by any proof. Instead, use ax-sep 2693 below so that the uses of the Axiom of Separation can be more easily identified.

Assertion

Ref	Expression
axsep	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

Distinct variable groups:   x,y,z   φ,y,z

Proof of Theorem axsep

Step	Hyp	Ref	Expression
1		ax-17 968	. . . 4 ⊢ ((w = x ⋀ φ) → ∀y(w = x ⋀ φ))
2	1	axrep5 2688	. . 3 ⊢ (∀w(w ∈ z → ∃y∀x((w = x ⋀ φ) → x = y)) → ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))))
3		a9e 1121	. . . . 5 ⊢ ∃y y = w
4		equtr 1127	. . . . . . . . 9 ⊢ (y = w → (w = x → y = x))
5		equcomi 1124	. . . . . . . . 9 ⊢ (y = x → x = y)
6	4, 5	syl6 22	. . . . . . . 8 ⊢ (y = w → (w = x → x = y))
7	6	adantrd 391	. . . . . . 7 ⊢ (y = w → ((w = x ⋀ φ) → x = y))
8	7	19.21aiv 1281	. . . . . 6 ⊢ (y = w → ∀x((w = x ⋀ φ) → x = y))
9	8	19.22i 1036	. . . . 5 ⊢ (∃y y = w → ∃y∀x((w = x ⋀ φ) → x = y))
10	3, 9	ax-mp 7	. . . 4 ⊢ ∃y∀x((w = x ⋀ φ) → x = y)
11	10	a1i 8	. . 3 ⊢ (w ∈ z → ∃y∀x((w = x ⋀ φ) → x = y))
12	2, 11	mpg 983	. 2 ⊢ ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
13		an12 483	. . . . . . 7 ⊢ ((w = x ⋀ (w ∈ z ⋀ φ)) ↔ (w ∈ z ⋀ (w = x ⋀ φ)))
14	13	exbii 1047	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
15		ax-17 968	. . . . . . 7 ⊢ ((x ∈ z ⋀ φ) → ∀w(x ∈ z ⋀ φ))
16		elequ1 1132	. . . . . . . 8 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
17	16	anbi1d 615	. . . . . . 7 ⊢ (w = x → ((w ∈ z ⋀ φ) ↔ (x ∈ z ⋀ φ)))
18	15, 17	equsex 1148	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ (x ∈ z ⋀ φ))
19	14, 18	bitr3 175	. . . . 5 ⊢ (∃w(w ∈ z ⋀ (w = x ⋀ φ)) ↔ (x ∈ z ⋀ φ))
20	19	bibi2i 606	. . . 4 ⊢ ((x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ (x ∈ y ↔ (x ∈ z ⋀ φ)))
21	20	albii 996	. . 3 ⊢ (∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ ∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
22	21	exbii 1047	. 2 ⊢ (∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
23	12, 22	mpbi 189	1 ⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ⋀ φ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃wex 977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-rep 2683

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain