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 4025. 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 2918. 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 4037, 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 4076 shows (contradicting zfauscl 4037). However, as axsep2 4036 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 4035 from axrep 4025. This theorem should not be referenced by any proof. Instead, use axsep 4035 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 1629  . . . 4  
2  1  axrep5 4030  . . 3 
3  equtr 1826  . . . . . . . 8  
4  equcomi 1822  . . . . . . . 8  
5  3, 4  syl6 31  . . . . . . 7 
6  5  adantrd 456  . . . . . 6 
7  6  alrimiv 2012  . . . . 5 
8  7  a1d 24  . . . 4 
9  8  a4imev 1997  . . 3 
10  2, 9  mpg 1542  . 2 
11  an12 775  . . . . . . 7  
12  11  exbii 1580  . . . . . 6 
13  nfv 1629  . . . . . . 7  
14  elequ1 1831  . . . . . . . 8  
15  14  anbi1d 688  . . . . . . 7 
16  13, 15  equsex 1852  . . . . . 6 
17  12, 16  bitr3i 244  . . . . 5 
18  17  bibi2i 306  . . . 4 
19  18  albii 1554  . . 3 
20  19  exbii 1580  . 2 
21  10, 20  mpbi 201  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wb 178 wa 360 wal 1532 wex 1537 wceq 1619 wcel 1621 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 ax5 1533 ax6 1534 ax7 1535 axgen 1536 ax8 1623 ax13 1625 ax14 1626 ax17 1628 ax9 1684 ax4 1692 axext 2234 axrep 4025 
This theorem depends on definitions: dfbi 179 dfan 362 dftru 1315 dfex 1538 dfnf 1540 dfcleq 2246 dfclel 2249 
Copyright terms: Public domain  W3C validator 