New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > isset | Unicode version |
Description: Two ways to say
" is a
set": A class
is a member of the
universal class (see df-v 2862) if and only if the class
exists (i.e. there exists some set equal to class ).
Theorem 6.9 of [Quine] p. 43.
Notational convention: We will use the
notational device " " to mean
" is a set"
very
frequently, for example in uniex 4318. Note the when is not a set,
it is called a proper class. In some theorems, such as uniexg 4317, in
order to shorten certain proofs we use the more general antecedent
instead of to mean
" is a
set."
Note that a constant is implicitly considered distinct from all variables. This is why is not included in the distinct variable list, even though df-clel 2349 requires that the expression substituted for not contain . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
isset |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clel 2349 | . 2 | |
2 | vex 2863 | . . . 4 | |
3 | 2 | biantru 491 | . . 3 |
4 | 3 | exbii 1582 | . 2 |
5 | 1, 4 | bitr4i 243 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wa 358 wex 1541 wceq 1642 wcel 1710 cvv 2860 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-v 2862 |
This theorem is referenced by: issetf 2865 isseti 2866 issetri 2867 elex 2868 elisset 2870 ceqex 2970 eueq 3009 moeq 3013 ru 3046 sbc5 3071 snprc 3789 ninexg 4098 snex 4112 1cex 4143 xpkvexg 4286 iotaex 4357 opeqexb 4621 eloprabga 5579 dmmpt 5684 fnce 6177 |
Copyright terms: Public domain | W3C validator |