Description: Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep , we invoke the Axiom of Extensionality (indirectly via vtocl ), which is needed for the justification of class variable notation.
If we omit the requirement that y not occur in ph , we can derive a contradiction, as notzfaus shows. (Contributed by NM, 21-Jun-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | zfauscl.1 | |- A e. _V |
|
| Assertion | zfauscl | |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfauscl.1 | |- A e. _V |
|
| 2 | eleq2 | |- ( z = A -> ( x e. z <-> x e. A ) ) |
|
| 3 | 2 | anbi1d | |- ( z = A -> ( ( x e. z /\ ph ) <-> ( x e. A /\ ph ) ) ) |
| 4 | 3 | bibi2d | |- ( z = A -> ( ( x e. y <-> ( x e. z /\ ph ) ) <-> ( x e. y <-> ( x e. A /\ ph ) ) ) ) |
| 5 | 4 | albidv | |- ( z = A -> ( A. x ( x e. y <-> ( x e. z /\ ph ) ) <-> A. x ( x e. y <-> ( x e. A /\ ph ) ) ) ) |
| 6 | 5 | exbidv | |- ( z = A -> ( E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) <-> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) ) ) |
| 7 | ax-sep | |- E. y A. x ( x e. y <-> ( x e. z /\ ph ) ) |
|
| 8 | 1 6 7 | vtocl | |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) |