HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem axsep 3453
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 3444. 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 2501. 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 3456, 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 3496 shows (contradicting zfauscl 3456). However, as axsep2 3455 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 3454 from ax-rep 3444.

This theorem should not be referenced by any proof. Instead, use ax-sep 3454 below so that the uses of the Axiom of Separation can be more easily identified.

Assertion
Ref Expression
axsep
Distinct variable groups:   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem axsep
StepHypRef Expression
1 ax-17 1441 . . . 4
21axrep5 3449 . . 3
3 a9e 1555 . . . . 5
4 equtr 1563 . . . . . . . . 9
5 equcomi 1560 . . . . . . . . 9
64, 5syl6 28 . . . . . . . 8
76adantrd 451 . . . . . . 7
87alrimiv 1719 . . . . . 6
98eximi 1373 . . . . 5
103, 9ax-mp 8 . . . 4
1110a1i 10 . . 3
122, 11mpg 1349 . 2
13 an12 742 . . . . . . 7
1413exbii 1380 . . . . . 6
15 ax-17 1441 . . . . . . 7
16 elequ1 1568 . . . . . . . 8
1716anbi1d 686 . . . . . . 7
1815, 17equsex 1580 . . . . . 6
1914, 18bitr3i 241 . . . . 5
2019bibi2i 304 . . . 4
2120albii 1361 . . 3
2221exbii 1380 . 2
2312, 22mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 360  wal 1341  wex 1346   wceq 1425   wcel 1427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-rep 3444
This theorem depends on definitions:  df-bi 175  df-an 362  df-ex 1347
Copyright terms: Public domain