![]() |
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 3330)
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 7106. Note that a class 𝐴 which
is
not a set is called a proper class. In some theorems, such as
uniexg 7108, 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 2744 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 2744 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 3331 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 527 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1911 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 267 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = wceq 1620 ∃wex 1841 ∈ wcel 2127 Vcvv 3328 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-12 2184 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-an 385 df-tru 1623 df-ex 1842 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-v 3330 |
This theorem is referenced by: issetf 3336 isseti 3337 issetri 3338 elex 3340 elisset 3343 vtoclg1f 3393 eueq 3507 moeq 3511 ru 3563 sbc5 3589 snprc 4385 vprc 4936 vnex 4938 eusvnfb 4999 reusv2lem3 5008 iotaex 6017 funimaexg 6124 fvmptd3f 6445 fvmptdv2 6448 ovmpt2df 6945 rankf 8818 isssc 16652 dmscut 32195 snelsingles 32306 bj-snglex 33238 bj-nul 33295 dissneqlem 33469 iotaexeu 39090 elnev 39110 ax6e2nd 39245 ax6e2ndVD 39612 ax6e2ndALT 39634 upbdrech 39987 itgsubsticclem 40663 |
Copyright terms: Public domain | W3C validator |