Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axsep | Structured version Visualization version GIF version |
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 4771. 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 3434. 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 4783, 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 4840 shows (contradicting zfauscl 4783). However, as axsep2 4782 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 4781 from ax-rep 4771. This theorem should not be referenced by any proof. Instead, use ax-sep 4781 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.) |
Ref | Expression |
---|---|
axsep | ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1843 | . . . 4 ⊢ Ⅎ𝑦(𝑤 = 𝑥 ∧ 𝜑) | |
2 | 1 | axrep5 4776 | . . 3 ⊢ (∀𝑤(𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))) |
3 | equtr 1948 | . . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑦 = 𝑥)) | |
4 | equcomi 1944 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
5 | 3, 4 | syl6 35 | . . . . . . 7 ⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑥 = 𝑦)) |
6 | 5 | adantrd 484 | . . . . . 6 ⊢ (𝑦 = 𝑤 → ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
7 | 6 | alrimiv 1855 | . . . . 5 ⊢ (𝑦 = 𝑤 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
8 | 7 | a1d 25 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝑤 ∈ 𝑧 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))) |
9 | 8 | spimev 2259 | . . 3 ⊢ (𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
10 | 2, 9 | mpg 1724 | . 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) |
11 | an12 838 | . . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) | |
12 | 11 | exbii 1774 | . . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) |
13 | elequ1 1997 | . . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) | |
14 | 13 | anbi1d 741 | . . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
15 | 14 | equsexvw 1932 | . . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
16 | 12, 15 | bitr3i 266 | . . . . 5 ⊢ (∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
17 | 16 | bibi2i 327 | . . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
18 | 17 | albii 1747 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
19 | 18 | exbii 1774 | . 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
20 | 10, 19 | mpbi 220 | 1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∀wal 1481 ∃wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-rep 4771 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |