Theorem axsep 2697

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 2688. 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 2700, 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 2736 shows (contradicting zfauscl 2700). However, as axsep2 2699 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 2698 from ax-rep 2688.

This theorem should not be referenced by any proof. Instead, use ax-sep 2698 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 2693	. . 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 ⋀ φ))

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 2688

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

Copyright terms: Public domain