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

Theorem axsep 4037
 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 4028. 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 2920. 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 4040, 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 4079 shows (contradicting zfauscl 4040). However, as axsep2 4039 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 4038 from ax-rep 4028. This theorem should not be referenced by any proof. Instead, use ax-sep 4038 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
StepHypRef Expression
1 nfv 1629 . . . 4
21axrep5 4033 . . 3
3 equtr 1826 . . . . . . . 8
4 equcomi 1822 . . . . . . . 8
53, 4syl6 31 . . . . . . 7
65adantrd 456 . . . . . 6
76alrimiv 2012 . . . . 5
87a1d 24 . . . 4
98a4imev 1997 . . 3
102, 9mpg 1542 . 2
11 an12 775 . . . . . . 7
1211exbii 1580 . . . . . 6
13 nfv 1629 . . . . . . 7
14 elequ1 1831 . . . . . . . 8
1514anbi1d 688 . . . . . . 7
1613, 15equsex 1852 . . . . . 6
1712, 16bitr3i 244 . . . . 5
1817bibi2i 306 . . . 4
1918albii 1554 . . 3
2019exbii 1580 . 2
2110, 20mpbi 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:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-13 1625  ax-14 1626  ax-17 1628  ax-9 1684  ax-4 1692  ax-ext 2234  ax-rep 4028 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-cleq 2246  df-clel 2249
 Copyright terms: Public domain W3C validator