Theorem axsep 2717

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 2708. 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 1945. 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 2720, 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 2756 shows (contradicting zfauscl 2720). However, as axsep2 2719 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 2718 from ax-rep 2708.

This theorem should not be referenced by any proof. Instead, use ax-sep 2718 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 975	. . . 4 ⊢ ((w = x ⋀ φ) → ∀y(w = x ⋀ φ))
2	1	axrep5 2713	. . 3 ⊢ (∀w(w ∈ z → ∃y∀x((w = x ⋀ φ) → x = y)) → ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))))
3		a9e 1129	. . . . 5 ⊢ ∃y y = w
4		equtr 1135	. . . . . . . . 9 ⊢ (y = w → (w = x → y = x))
5		equcomi 1132	. . . . . . . . 9 ⊢ (y = x → x = y)
6	4, 5	syl6 22	. . . . . . . 8 ⊢ (y = w → (w = x → x = y))
7	6	adantrd 393	. . . . . . 7 ⊢ (y = w → ((w = x ⋀ φ) → x = y))
8	7	19.21aiv 1290	. . . . . 6 ⊢ (y = w → ∀x((w = x ⋀ φ) → x = y))
9	8	19.22i 1044	. . . . 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 990	. 2 ⊢ ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
13		an12 487	. . . . . . 7 ⊢ ((w = x ⋀ (w ∈ z ⋀ φ)) ↔ (w ∈ z ⋀ (w = x ⋀ φ)))
14	13	exbii 1055	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
15		ax-17 975	. . . . . . 7 ⊢ ((x ∈ z ⋀ φ) → ∀w(x ∈ z ⋀ φ))
16		elequ1 1140	. . . . . . . 8 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
17	16	anbi1d 620	. . . . . . 7 ⊢ (w = x → ((w ∈ z ⋀ φ) ↔ (x ∈ z ⋀ φ)))
18	15, 17	equsex 1156	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ (x ∈ z ⋀ φ))
19	14, 18	bitr3i 175	. . . . 5 ⊢ (∃w(w ∈ z ⋀ (w = x ⋀ φ)) ↔ (x ∈ z ⋀ φ))
20	19	bibi2i 611	. . . 4 ⊢ ((x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ (x ∈ y ↔ (x ∈ z ⋀ φ)))
21	20	albii 1003	. . 3 ⊢ (∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ ∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
22	21	exbii 1055	. 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 958   = wceq 960   ∈ wcel 962  ∃wex 984

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-rep 2708

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

Copyright terms: Public domain