HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1803) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A ∈ V" to mean "A is a set" very frequently, for example in uniex 2861. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 2862, in order to shorten certain proofs we use the more general antecedent A ∈ B instead of A ∈ V to mean "A is a set." |
| Ref | Expression |
|---|---|
| isset | ⊢ (A ∈ V ↔ ∃x x = A) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-clel 1465 | . 2 ⊢ (A ∈ V ↔ ∃x(x = A ⋀ x ∈ V)) | |
| 2 | visset 1804 | . . . 4 ⊢ x ∈ V | |
| 3 | 2 | biantru 722 | . . 3 ⊢ (x = A ↔ (x = A ⋀ x ∈ V)) |
| 4 | 3 | exbii 1047 | . 2 ⊢ (∃x x = A ↔ ∃x(x = A ⋀ x ∈ V)) |
| 5 | 1, 4 | bitr4 176 | 1 ⊢ (A ∈ V ↔ ∃x x = A) |
| Colors of variables: wff set class |
| Syntax hints: ↔ wb 146 ⋀ wa 223 = wceq 953 ∈ wcel 955 ∃wex 977 Vcvv 1802 |
| This theorem is referenced by: isseti 1806 issetri 1807 elisset 1808 elex 1810 vtoclgf 1837 cla4gf 1851 ceqex 1877 eueq 1907 moeq 1911 ru 1928 elrabsf 1953 snprc 2433 nvelv 2703 vnex 2705 dmsnop 3317 funimaexg 3561 isarep2 3564 fopab2 3808 tz9.12lem1 4631 tz9.12lem3 4633 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 960 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-ext 1452 |
| This theorem depends on definitions: df-bi 147 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-v 1803 |