Theorem axsep 5018

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 5008. 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 𝑥 ∈ 𝑧) so that it asserts the existence of a collection only if it is smaller than some other collection 𝑧 that already exists. This prevents Russell's paradox ru 3651. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

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

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

If we omit the requirement that 𝑦 not occur in 𝜑, we can derive a contradiction, as notzfaus 5076 shows (showing the necessity of that condition in zfauscl 5021). However, as axsep2 5020 shows, we can eliminate the restriction that 𝑧 not occur in 𝜑.

Note: the distinct variable restriction that 𝑧 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 5019 from ax-rep 5008.

This theorem should not be referenced by any proof. Instead, use ax-sep 5019 below so that the uses of the Axiom of Separation can be more easily identified. (Contributed by NM, 11-Sep-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
axsep	⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦,𝑧

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem axsep

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1957	. . . 4 ⊢ Ⅎ𝑦(𝑤 = 𝑥 ∧ 𝜑)
2	1	axrep5 5014	. . 3 ⊢ (∀𝑤(𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))))
3		equtr 2068	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑦 = 𝑥))
4		equcomi 2064	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
5	3, 4	syl6 35	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑥 = 𝑦))
6	5	adantrd 487	. . . . . 6 ⊢ (𝑦 = 𝑤 → ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
7	6	alrimiv 1970	. . . . 5 ⊢ (𝑦 = 𝑤 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
8	7	a1d 25	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑤 ∈ 𝑧 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)))
9	8	spimev 2357	. . 3 ⊢ (𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
10	2, 9	mpg 1841	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11		an12 635	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12	11	exbii 1892	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
13		elequ1 2114	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
14	13	anbi1d 623	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
15	14	equsexvw 2052	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	12, 15	bitr3i 269	. . . . 5 ⊢ (∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
17	16	bibi2i 329	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	albii 1863	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	18	exbii 1892	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
20	10, 19	mpbi 222	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599  ∃wex 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-rep 5008

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828

This theorem is referenced by: (None)