axsep - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem axsep 2698

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 2689. 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 1934. 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 2701, 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 2737 shows (contradicting zfauscl 2701). However, as axsep2 2700 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 2699 from ax-rep 2689.

This theorem should not be referenced by any proof. Instead, use ax-sep 2699 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 969	. . . 4 ⊢ ((w = x ⋀ φ) → ∀y(w = x ⋀ φ))
2	1	axrep5 2694	. . 3 ⊢ (∀w(w ∈ z → ∃y∀x((w = x ⋀ φ) → x = y)) → ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))))
3		a9e 1123	. . . . 5 ⊢ ∃y y = w
4		equtr 1129	. . . . . . . . 9 ⊢ (y = w → (w = x → y = x))
5		equcomi 1126	. . . . . . . . 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 1284	. . . . . 6 ⊢ (y = w → ∀x((w = x ⋀ φ) → x = y))
9	8	19.22i 1038	. . . . 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 984	. 2 ⊢ ∃y∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
13		an12 484	. . . . . . 7 ⊢ ((w = x ⋀ (w ∈ z ⋀ φ)) ↔ (w ∈ z ⋀ (w = x ⋀ φ)))
14	13	exbii 1049	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ)))
15		ax-17 969	. . . . . . 7 ⊢ ((x ∈ z ⋀ φ) → ∀w(x ∈ z ⋀ φ))
16		elequ1 1134	. . . . . . . 8 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
17	16	anbi1d 616	. . . . . . 7 ⊢ (w = x → ((w ∈ z ⋀ φ) ↔ (x ∈ z ⋀ φ)))
18	15, 17	equsex 1150	. . . . . 6 ⊢ (∃w(w = x ⋀ (w ∈ z ⋀ φ)) ↔ (x ∈ z ⋀ φ))
19	14, 18	bitr3 175	. . . . 5 ⊢ (∃w(w ∈ z ⋀ (w = x ⋀ φ)) ↔ (x ∈ z ⋀ φ))
20	19	bibi2i 607	. . . 4 ⊢ ((x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ (x ∈ y ↔ (x ∈ z ⋀ φ)))
21	20	albii 997	. . 3 ⊢ (∀x(x ∈ y ↔ ∃w(w ∈ z ⋀ (w = x ⋀ φ))) ↔ ∀x(x ∈ y ↔ (x ∈ z ⋀ φ)))
22	21	exbii 1049	. 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 ⋀ φ))

Colors of variables: wff set class

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

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-9 963 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-rep 2689

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