Home | Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode 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 3456. 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 2492. 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 3468, which requires the Axiom of Extensionality as well as Replacement for its derivation. If we omit the requirement that not occur in , we can derive a contradiction, as notzfaus 3508 shows (contradicting zfauscl 3468). However, as axsep2 3467 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 3466 from ax-rep 3456. This theorem should not be referenced by any proof. Instead, use ax-sep 3466 below so that the uses of the Axiom of Separation can be more easily identified. |
Ref | Expression |
---|---|
axsep |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1430 | . . . 4 | |
2 | 1 | axrep5 3461 | . . 3 |
3 | a9e 1544 | . . . 4 | |
4 | equtr 1552 | . . . . . . . 8 | |
5 | equcomi 1549 | . . . . . . . 8 | |
6 | 4, 5 | syl6 29 | . . . . . . 7 |
7 | 6 | adantrd 447 | . . . . . 6 |
8 | 7 | alrimiv 1708 | . . . . 5 |
9 | 8 | eximi 1362 | . . . 4 |
10 | 3, 9 | mp1i 11 | . . 3 |
11 | 2, 10 | mpg 1338 | . 2 |
12 | an12 734 | . . . . . . 7 | |
13 | 12 | exbii 1369 | . . . . . 6 |
14 | ax-17 1430 | . . . . . . 7 | |
15 | elequ1 1557 | . . . . . . . 8 | |
16 | 15 | anbi1d 679 | . . . . . . 7 |
17 | 14, 16 | equsex 1569 | . . . . . 6 |
18 | 13, 17 | bitr3i 240 | . . . . 5 |
19 | 18 | bibi2i 302 | . . . 4 |
20 | 19 | albii 1350 | . . 3 |
21 | 20 | exbii 1369 | . 2 |
22 | 11, 21 | mpbi 197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 174 wa 357 wal 1330 wex 1335 wceq 1414 wcel 1416 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-5 1331 ax-6 1332 ax-7 1333 ax-gen 1334 ax-8 1418 ax-13 1422 ax-14 1423 ax-17 1430 ax-9 1445 ax-4 1451 ax-rep 3456 |
This theorem depends on definitions: df-bi 175 df-an 359 df-ex 1336 |