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 4133. 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 2992. 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 4145, 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 4187 shows (contradicting zfauscl 4145). However, as axsep2 4144 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 4143 from axrep 4133. This theorem should not be referenced by any proof. Instead, use axsep 4143 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 1607  . . . 4  
2  1  axrep5 4138  . . 3 
3  equtr 1654  . . . . . . . 8  
4  equcomi 1648  . . . . . . . 8  
5  3, 4  syl6 29  . . . . . . 7 
6  5  adantrd 454  . . . . . 6 
7  6  alrimiv 1619  . . . . 5 
8  7  a1d 22  . . . 4 
9  8  spimev 1941  . . 3 
10  2, 9  mpg 1537  . 2 
11  an12 772  . . . . . . 7  
12  11  exbii 1571  . . . . . 6 
13  nfv 1607  . . . . . . 7  
14  elequ1 1689  . . . . . . . 8  
15  14  anbi1d 685  . . . . . . 7 
16  13, 15  equsex 1904  . . . . . 6 
17  12, 16  bitr3i 242  . . . . 5 
18  17  bibi2i 304  . . . 4 
19  18  albii 1555  . . 3 
20  19  exbii 1571  . 2 
21  10, 20  mpbi 199  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 176 wa 358 wal 1529 wex 1530 wceq 1625 wcel 1686 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1535 ax5 1546 ax17 1605 ax9 1637 ax8 1645 ax13 1688 ax14 1690 ax6 1705 ax7 1710 ax11 1717 ax12 1868 axext 2266 axrep 4133 
This theorem depends on definitions: dfbi 177 dfan 360 dftru 1310 dfex 1531 dfnf 1534 dfcleq 2278 dfclel 2281 
Copyright terms: Public domain  W3C validator 