Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axsep | Structured version Visualization version 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 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 |