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.

Step	Hyp	Ref	Expression
1		nfv 1707	. . . 4
2	1	axrep5 4568	. . 3
3		equtr 1796	. . . . . . . 8
4		equcomi 1793	. . . . . . . 8
5	3, 4	syl6 33	. . . . . . 7
6	5	adantrd 468	. . . . . 6
7	6	alrimiv 1719	. . . . 5
8	7	a1d 25	. . . 4
9	8	spimev 2010	. . 3
10	2, 9	mpg 1620	. 2
11		an12 797	. . . . . . 7
12	11	exbii 1667	. . . . . 6
13		nfv 1707	. . . . . . 7
14		elequ1 1821	. . . . . . . 8
15	14	anbi1d 704	. . . . . . 7
16	13, 15	equsex 2038	. . . . . 6
17	12, 16	bitr3i 251	. . . . 5
18	17	bibi2i 313	. . . 4
19	18	albii 1640	. . 3
20	19	exbii 1667	. 2
21	10, 20	mpbi 208	1

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