![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isset | Structured version Visualization version GIF version |
Description: Two ways to say
"𝐴 is a set": A class 𝐴 is a
member of the
universal class V (see df-v 3399)
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 "𝐴 ∈ V " to mean "𝐴 is a
set" very
frequently, for example in uniex 7230. Note that a class 𝐴 which
is
not a set is called a proper class. In some theorems, such as
uniexg 7232, in order to shorten certain proofs we use
the more general
antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean
"𝐴 is a set."
Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2773 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 | ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clel 2773 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 3400 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 525 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1892 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 270 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 = wceq 1601 ∃wex 1823 ∈ wcel 2106 Vcvv 3397 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1605 df-ex 1824 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-v 3399 |
This theorem is referenced by: issetf 3409 isseti 3410 issetri 3411 elex 3413 elisset 3416 vtoclg1f 3465 eueq 3588 eueqOLD 3589 moeqOLD 3593 ru 3650 sbc5 3676 snprc 4483 vprc 5034 eusvnfb 5105 reusv2lem3 5112 iotaex 6116 funimaexg 6220 fvmptd3f 6556 fvmptdv2 6559 ovmpt2df 7069 rankf 8954 isssc 16865 dmscut 32521 snelsingles 32632 bj-snglex 33547 bj-nul 33604 dissneqlem 33797 iotaexeu 39566 elnev 39586 ax6e2nd 39710 ax6e2ndVD 40069 ax6e2ndALT 40091 upbdrech 40420 itgsubsticclem 41110 |
Copyright terms: Public domain | W3C validator |