![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isset | Structured version Visualization version GIF version |
Description: Two ways to express that
"𝐴 is a set": A class 𝐴 is a
member
of the universal class V (see df-v 3464)
if and only if the class
𝐴 exists (i.e., there exists some set
𝑥
equal to class 𝐴).
Theorem 6.9 of [Quine] p. 43.
A class 𝐴 which is not a set is called a proper class. Conventions: We will often use the expression "𝐴 ∈ V " to mean "𝐴 is a set", for example in uniex 7744. To make some theorems more readily applicable, we will also use the more general expression 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg 7743 compared with uniex 7744). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3482. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
isset | ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3466 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | issetlem 2806 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1534 ∃wex 1774 ∈ wcel 2099 Vcvv 3462 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 |
This theorem is referenced by: issetft 3477 issetri 3480 elex 3482 elexOLD 3483 eueq 3701 ru 3773 ruOLD 3774 sbc5ALT 3804 snprc 4716 snssb 4781 vprc 5312 eusvnfb 5389 reusv2lem3 5396 iotaexOLD 6526 funimaexgOLD 6638 fvmptd3f 7016 fvmptdv2 7019 ovmpodf 7574 rankf 9830 fnpr2ob 17568 isssc 17831 lrrecfr 27954 snelsingles 35759 bj-snglex 36693 bj-abex 36750 bj-clex 36751 bj-nul 36776 dissneqlem 37060 wl-issetft 37290 snen1g 43228 rr-spce 43908 iotaexeu 44129 elnev 44149 ax6e2nd 44271 ax6e2ndVD 44621 ax6e2ndALT 44643 upbdrech 44956 itgsubsticclem 45632 |
Copyright terms: Public domain | W3C validator |