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

Theorem axsep 3686
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 3677. 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 2668. 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 3689, 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 3729 shows (contradicting zfauscl 3689). However, as axsep2 3688 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 3687 from ax-rep 3677.

This theorem should not be referenced by any proof. Instead, use ax-sep 3687 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 1542 . . . 4
21axrep5 3682 . . 3
3 a9e 1696 . . . 4
4 equtr 1704 . . . . . . . 8
5 equcomi 1701 . . . . . . . 8
64, 5syl6 29 . . . . . . 7
76adantrd 447 . . . . . 6
87alrimiv 1873 . . . . 5
98eximi 1479 . . . 4
103, 9mp1i 11 . . 3
112, 10mpg 1453 . 2
12 an12 734 . . . . . . 7
1312exbii 1486 . . . . . 6
14 ax-17 1542 . . . . . . 7
15 elequ1 1709 . . . . . . . 8
1615anbi1d 679 . . . . . . 7
1714, 16equsex 1726 . . . . . 6
1813, 17bitr3i 240 . . . . 5
1918bibi2i 302 . . . 4
2019albii 1465 . . 3
2120exbii 1486 . 2
2211, 21mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357  wal 1445  wex 1450   wceq 1531   wcel 1533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-4 1605  ax-rep 3677
This theorem depends on definitions:  df-bi 175  df-an 359  df-ex 1451
Copyright terms: Public domain