# Metamath Proof Explorer

## Theorem zfauscl

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}\in \mathrm{V}$
Assertion zfauscl ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {A}\wedge {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 zfauscl.1 ${⊢}{A}\in \mathrm{V}$
2 eleq2 ${⊢}{z}={A}\to \left({x}\in {z}↔{x}\in {A}\right)$
3 2 anbi1d ${⊢}{z}={A}\to \left(\left({x}\in {z}\wedge {\phi }\right)↔\left({x}\in {A}\wedge {\phi }\right)\right)$
4 3 bibi2d ${⊢}{z}={A}\to \left(\left({x}\in {y}↔\left({x}\in {z}\wedge {\phi }\right)\right)↔\left({x}\in {y}↔\left({x}\in {A}\wedge {\phi }\right)\right)\right)$
5 4 albidv ${⊢}{z}={A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {z}\wedge {\phi }\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {A}\wedge {\phi }\right)\right)\right)$
6 5 exbidv ${⊢}{z}={A}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {z}\wedge {\phi }\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {A}\wedge {\phi }\right)\right)\right)$
7 ax-sep ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {z}\wedge {\phi }\right)\right)$
8 1 6 7 vtocl ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}↔\left({x}\in {A}\wedge {\phi }\right)\right)$