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

Theorem zfauscl 4526
 Description: Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4524, we invoke the Axiom of Extensionality (indirectly via vtocl 3130), 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 4578 shows. (Contributed by NM, 21-Jun-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 2527 . . . . . 6
32anbi1d 704 . . . . 5
43bibi2d 318 . . . 4
54albidv 1680 . . 3
65exbidv 1681 . 2
7 ax-sep 4524 . 2
81, 6, 7vtocl 3130 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369  wal 1368   wceq 1370  wex 1587   wcel 1758  cvv 3078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-ext 2432  ax-sep 4524 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080 This theorem is referenced by:  inex1  4544
 Copyright terms: Public domain W3C validator