![]() |
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 3445)
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 7674. 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 7673 compared with uniex 7674). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3461. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
isset | ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3447 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | issetlem 2817 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 ∃wex 1781 ∈ wcel 2106 Vcvv 3443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 |
This theorem is referenced by: issetf 3457 issetri 3459 elex 3461 eueq 3664 ru 3736 sbc5ALT 3766 snprc 4676 snssb 4741 vprc 5270 eusvnfb 5346 reusv2lem3 5353 iotaexOLD 6473 funimaexgOLD 6585 fvmptd3f 6960 fvmptdv2 6963 ovmpodf 7507 rankf 9726 fnpr2ob 17432 isssc 17695 lrrecfr 27239 snelsingles 34474 bj-snglex 35411 bj-abex 35468 bj-clex 35469 bj-nul 35494 dissneqlem 35778 wl-issetft 36001 snen1g 41738 rr-spce 42419 iotaexeu 42640 elnev 42660 ax6e2nd 42782 ax6e2ndVD 43132 ax6e2ndALT 43154 upbdrech 43475 itgsubsticclem 44148 |
Copyright terms: Public domain | W3C validator |