Theorem axsep 4708

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 4699. 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 3401. 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 4711, 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 4766 shows (contradicting zfauscl 4711). However, as axsep2 4710 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 4709 from ax-rep 4699.

This theorem should not be referenced by any proof. Instead, use ax-sep 4709 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 1830	. . . 4 ⊢ Ⅎ𝑦(𝑤 = 𝑥 ∧ 𝜑)
2	1	axrep5 4704	. . 3 ⊢ (∀𝑤(𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))))
3		equtr 1935	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑦 = 𝑥))
4		equcomi 1931	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
5	3, 4	syl6 34	. . . . . . 7 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑥 = 𝑦))
6	5	adantrd 483	. . . . . 6 ⊢ (𝑦 = 𝑤 → ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
7	6	alrimiv 1842	. . . . 5 ⊢ (𝑦 = 𝑤 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
8	7	a1d 25	. . . 4 ⊢ (𝑦 = 𝑤 → (𝑤 ∈ 𝑧 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)))
9	8	spimev 2247	. . 3 ⊢ (𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))
10	2, 9	mpg 1715	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11		an12 834	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12	11	exbii 1764	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
13		elequ1 1984	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
14	13	anbi1d 737	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
15	14	equsexvw 1919	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	12, 15	bitr3i 265	. . . . 5 ⊢ (∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
17	16	bibi2i 326	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	albii 1737	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	18	exbii 1764	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
20	10, 19	mpbi 219	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-rep 4699

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by: (None)