Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axsep Unicode version

Theorem axsep 4140
 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 4131. 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 2990. 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 4143, 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 4185 shows (contradicting zfauscl 4143). However, as axsep2 4142 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 4141 from ax-rep 4131. This theorem should not be referenced by any proof. Instead, use ax-sep 4141 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.)
Assertion
Ref Expression
axsep
Distinct variable groups:   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem axsep
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1605 . . . 4
21axrep5 4136 . . 3
3 equtr 1652 . . . . . . . 8
4 equcomi 1646 . . . . . . . 8
53, 4syl6 29 . . . . . . 7
65adantrd 454 . . . . . 6
76alrimiv 1617 . . . . 5
87a1d 22 . . . 4
98spimev 1939 . . 3
102, 9mpg 1535 . 2
11 an12 772 . . . . . . 7
1211exbii 1569 . . . . . 6
13 nfv 1605 . . . . . . 7
14 elequ1 1687 . . . . . . . 8
1514anbi1d 685 . . . . . . 7
1613, 15equsex 1902 . . . . . 6
1712, 16bitr3i 242 . . . . 5
1817bibi2i 304 . . . 4
1918albii 1553 . . 3
2019exbii 1569 . 2
2110, 20mpbi 199 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wal 1527  wex 1528   wceq 1623   wcel 1684 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-cleq 2276  df-clel 2279
 Copyright terms: Public domain W3C validator