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 2490. 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 1429 . . . 4
21axrep5 3449 . . 3
3 a9e 1543 . . . . 5
4 equtr 1551 . . . . . . . . 9
5 equcomi 1548 . . . . . . . . 9
64, 5syl6 28 . . . . . . . 8
76adantrd 446 . . . . . . 7
87alrimiv 1707 . . . . . 6
98eximi 1361 . . . . 5
103, 9ax-mp 8 . . . 4
1110a1i 10 . . 3
122, 11mpg 1337 . 2
13 an12 733 . . . . . . 7
1413exbii 1368 . . . . . 6
15 ax-17 1429 . . . . . . 7
16 elequ1 1556 . . . . . . . 8
1716anbi1d 678 . . . . . . 7
1815, 17equsex 1568 . . . . . 6
1914, 18bitr3i 239 . . . . 5
2019bibi2i 301 . . . 4
2120albii 1349 . . 3
2221exbii 1368 . 2
2312, 22mpbi 196 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 173   wa 356  wal 1329  wex 1334   wceq 1413   wcel 1415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-rep 3444
This theorem depends on definitions:  df-bi 174  df-an 358  df-ex 1335
Copyright terms: Public domain