Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > zfauscl | Structured version Visualization version Unicode version |
Description: Separation Scheme
(Aussonderung) using a class variable. To derive this
from ax-sep 4781, we invoke the Axiom of Extensionality
(indirectly via
vtocl 3259), 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 4840 shows. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
zfauscl.1 |
Ref | Expression |
---|---|
zfauscl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfauscl.1 | . 2 | |
2 | eleq2 2690 | . . . . . 6 | |
3 | 2 | anbi1d 741 | . . . . 5 |
4 | 3 | bibi2d 332 | . . . 4 |
5 | 4 | albidv 1849 | . . 3 |
6 | 5 | exbidv 1850 | . 2 |
7 | ax-sep 4781 | . 2 | |
8 | 1, 6, 7 | vtocl 3259 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wal 1481 wceq 1483 wex 1704 wcel 1990 cvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-12 2047 ax-ext 2602 ax-sep 4781 |
This theorem depends on definitions: df-bi 197 df-an 386 df-tru 1486 df-ex 1705 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 |
This theorem is referenced by: inex1 4799 |
Copyright terms: Public domain | W3C validator |