Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zfauscl Structured version   Unicode version

Theorem zfauscl 4334
 Description: Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4332, we invoke the Axiom of Extensionality (indirectly via vtocl 3008), which is needed for the justification of class variable notation. If we omit the requirement that not occur in , we can derive a contradiction, as notzfaus 4376 shows. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
zfauscl.1
Assertion
Ref Expression
zfauscl
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem zfauscl
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 zfauscl.1 . 2
2 eleq2 2499 . . . . . 6
32anbi1d 687 . . . . 5
43bibi2d 311 . . . 4
54albidv 1636 . . 3
65exbidv 1637 . 2
7 ax-sep 4332 . 2
81, 6, 7vtocl 3008 1
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360  wal 1550  wex 1551   wceq 1653   wcel 1726  cvv 2958 This theorem is referenced by:  inex1  4346 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762  ax-ext 2419  ax-sep 4332 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960
 Copyright terms: Public domain W3C validator