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 3616. 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 2608. 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 3628, 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 3668 shows (contradicting zfauscl 3628). However, as axsep2 3627 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 3626 from ax-rep 3616. This theorem should not be referenced by any proof. Instead, use ax-sep 3626 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 1542 | . . . 4 | |
2 | 1 | axrep5 3621 | . . 3 |
3 | a9e 1656 | . . . 4 | |
4 | equtr 1664 | . . . . . . . 8 | |
5 | equcomi 1661 | . . . . . . . 8 | |
6 | 4, 5 | syl6 29 | . . . . . . 7 |
7 | 6 | adantrd 447 | . . . . . 6 |
8 | 7 | alrimiv 1820 | . . . . 5 |
9 | 8 | eximi 1474 | . . . 4 |
10 | 3, 9 | mp1i 11 | . . 3 |
11 | 2, 10 | mpg 1450 | . 2 |
12 | an12 734 | . . . . . . 7 | |
13 | 12 | exbii 1481 | . . . . . 6 |
14 | ax-17 1542 | . . . . . . 7 | |
15 | elequ1 1669 | . . . . . . . 8 | |
16 | 15 | anbi1d 679 | . . . . . . 7 |
17 | 14, 16 | equsex 1681 | . . . . . 6 |
18 | 13, 17 | bitr3i 240 | . . . . 5 |
19 | 18 | bibi2i 302 | . . . 4 |
20 | 19 | albii 1462 | . . 3 |
21 | 20 | exbii 1481 | . 2 |
22 | 11, 21 | mpbi 197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 174 wa 357 wal 1442 wex 1447 wceq 1526 wcel 1528 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-5 1443 ax-6 1444 ax-7 1445 ax-gen 1446 ax-8 1530 ax-13 1534 ax-14 1535 ax-17 1542 ax-9 1557 ax-4 1563 ax-rep 3616 |
This theorem depends on definitions: df-bi 175 df-an 359 df-ex 1448 |