Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE 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 2559) 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 4174. Note the when is not a set,
it is called a proper class. In some theorems, such as uniexg 4175, 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 2036 requires that the expression substituted for not contain . (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
isset |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clel 2036 | . 2 | |
2 | vex 2560 | . . . 4 | |
3 | 2 | biantru 286 | . . 3 |
4 | 3 | exbii 1496 | . 2 |
5 | 1, 4 | bitr4i 176 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 wceq 1243 wex 1381 wcel 1393 cvv 2557 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-v 2559 |
This theorem is referenced by: issetf 2562 isseti 2563 issetri 2564 elex 2566 elisset 2568 ceqex 2671 eueq 2712 moeq 2716 mosubt 2718 ru 2763 sbc5 2787 snprc 3435 vprc 3888 vnex 3890 opelopabsb 3997 eusvnfb 4186 dtruex 4283 euiotaex 4883 fvmptdf 5258 fvmptdv2 5260 fmptco 5330 brabvv 5551 ovmpt2df 5632 ovi3 5637 tfrlemibxssdm 5941 freccl 5993 ecexr 6111 bj-vprc 10016 bj-vnex 10018 bj-2inf 10062 |
Copyright terms: Public domain | W3C validator |