Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axsep  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 axrep 4263. 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 3105. 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 4275, 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 4317 shows (contradicting zfauscl 4275). However, as axsep2 4274 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 axsep 4273 from axrep 4263. This theorem should not be referenced by any proof. Instead, use axsep 4273 below so that the uses of the Axiom of Separation can be more easily identified. (Contributed by NM, 11Sep2006.) (New usage is discouraged.) 
Ref  Expression 

axsep 
Step  Hyp  Ref  Expression 

1  nfv 1626  . . . 4  
2  1  axrep5 4268  . . 3 
3  equtr 1689  . . . . . . . 8  
4  equcomi 1686  . . . . . . . 8  
5  3, 4  syl6 31  . . . . . . 7 
6  5  adantrd 455  . . . . . 6 
7  6  alrimiv 1638  . . . . 5 
8  7  a1d 23  . . . 4 
9  8  spimev 1955  . . 3 
10  2, 9  mpg 1554  . 2 
11  an12 773  . . . . . . 7  
12  11  exbii 1589  . . . . . 6 
13  nfv 1626  . . . . . . 7  
14  elequ1 1720  . . . . . . . 8  
15  14  anbi1d 686  . . . . . . 7 
16  13, 15  equsex 1962  . . . . . 6 
17  12, 16  bitr3i 243  . . . . 5 
18  17  bibi2i 305  . . . 4 
19  18  albii 1572  . . 3 
20  19  exbii 1589  . 2 
21  10, 20  mpbi 200  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 wa 359 wal 1546 wex 1547 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1552 ax5 1563 ax17 1623 ax9 1661 ax8 1682 ax13 1719 ax14 1721 ax6 1736 ax7 1741 ax11 1753 ax12 1939 axrep 4263 
This theorem depends on definitions: dfbi 178 dfan 361 dftru 1325 dfex 1548 dfnf 1551 
Copyright terms: Public domain  W3C validator 