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 3715. 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 2680. 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 3727, 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 3767 shows (contradicting zfauscl 3727). However, as axsep2 3726 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 3725 from ax-rep 3715. This theorem should not be referenced by any proof. Instead, use ax-sep 3725 below so that the uses of the Axiom of Separation can be more easily identified. (Contributed by NM, 11-Sep-2006.) |
Ref | Expression |
---|---|
axsep |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1547 | . . . 4 | |
2 | 1 | axrep5 3720 | . . 3 |
3 | a9e 1701 | . . . 4 | |
4 | equtr 1709 | . . . . . . . 8 | |
5 | equcomi 1706 | . . . . . . . 8 | |
6 | 4, 5 | syl6 29 | . . . . . . 7 |
7 | 6 | adantrd 448 | . . . . . 6 |
8 | 7 | alrimiv 1878 | . . . . 5 |
9 | 8 | eximi 1484 | . . . 4 |
10 | 3, 9 | mp1i 11 | . . 3 |
11 | 2, 10 | mpg 1458 | . 2 |
12 | an12 734 | . . . . . . 7 | |
13 | 12 | exbii 1491 | . . . . . 6 |
14 | ax-17 1547 | . . . . . . 7 | |
15 | elequ1 1714 | . . . . . . . 8 | |
16 | 15 | anbi1d 679 | . . . . . . 7 |
17 | 14, 16 | equsex 1731 | . . . . . 6 |
18 | 13, 17 | bitr3i 240 | . . . . 5 |
19 | 18 | bibi2i 302 | . . . 4 |
20 | 19 | albii 1470 | . . 3 |
21 | 20 | exbii 1491 | . 2 |
22 | 11, 21 | mpbi 197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 174 wa 357 wal 1450 wex 1455 wceq 1536 wcel 1538 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-5 1451 ax-6 1452 ax-7 1453 ax-gen 1454 ax-8 1540 ax-13 1543 ax-14 1544 ax-17 1547 ax-9 1568 ax-4 1610 ax-rep 3715 |
This theorem depends on definitions: df-bi 175 df-an 359 df-ex 1456 |