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

Theorem axsep 4572
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 4563. 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 3326. 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 (x). 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 4575, 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 4627 shows (contradicting zfauscl 4575). However, as axsep2 4574 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 4573 from ax-rep 4563.

This theorem should not be referenced by any proof. Instead, use ax-sep 4573 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:   , ,   , ,

Proof of Theorem axsep
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1707 . . . 4
21axrep5 4568 . . 3
3 equtr 1796 . . . . . . . 8
4 equcomi 1793 . . . . . . . 8
53, 4syl6 33 . . . . . . 7
65adantrd 468 . . . . . 6
76alrimiv 1719 . . . . 5
87a1d 25 . . . 4
98spimev 2010 . . 3
102, 9mpg 1620 . 2
11 an12 797 . . . . . . 7
1211exbii 1667 . . . . . 6
13 nfv 1707 . . . . . . 7
14 elequ1 1821 . . . . . . . 8
1514anbi1d 704 . . . . . . 7
1613, 15equsex 2038 . . . . . 6
1712, 16bitr3i 251 . . . . 5
1817bibi2i 313 . . . 4
1918albii 1640 . . 3
2019exbii 1667 . 2
2110, 20mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-rep 4563
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator