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 V
Assertion zfauscl y x x y x A φ


Step Hyp Ref Expression
1 zfauscl.1 A V
2 eleq2 z = A x z x A
3 2 anbi1d z = A x z φ x A φ
4 3 bibi2d z = A x y x z φ x y x A φ
5 4 albidv z = A x x y x z φ x x y x A φ
6 5 exbidv z = A y x x y x z φ y x x y x A φ
7 ax-sep y x x y x z φ
8 1 6 7 vtocl y x x y x A φ