HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Axiom ax-sep 2693
Description: The Axiom of Separation of ZF set theory. It was derived as axsep 2692 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
Assertion
Ref Expression
ax-sep |- E.yA.x(x e. y <-> (x e. z /\ ph))
Distinct variable groups:   x,y,z   ph,y,z
Detailed syntax breakdown of Axiom ax-sep
StepHypRef Expression
1 vx . . . . . 6 set x
21cv 952 . . . . 5 class x
3 vy . . . . . 6 set y
43cv 952 . . . . 5 class y
52, 4wcel 955 . . . 4 wff x e. y
6 vz . . . . . . 7 set z
76cv 952 . . . . . 6 class z
82, 7wcel 955 . . . . 5 wff x e. z
9 wph . . . . 5 wff ph
108, 9wa 223 . . . 4 wff (x e. z /\ ph)
115, 10wb 146 . . 3 wff (x e. y <-> (x e. z /\ ph))
1211, 1wal 951 . 2 wff A.x(x e. y <-> (x e. z /\ ph))
1312, 3wex 977 1 wff E.yA.x(x e. y <-> (x e. z /\ ph))
Colors of variables: wff set class
This axiom is referenced by:  axsep2 2694  zfauscl 2695  bm1.3ii 2696  axnul 2699
Copyright terms: Public domain