![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > isset | GIF version |
Description: Two ways to say
"𝐴 is a set": A class 𝐴 is a
member of the
universal class V (see df-v 2635)
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 4288. Note the when 𝐴 is not
a set,
it is called a proper class. In some theorems, such as uniexg 4290, 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 2091 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 2091 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 2636 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 297 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1548 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 186 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 = wceq 1296 ∃wex 1433 ∈ wcel 1445 Vcvv 2633 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-v 2635 |
This theorem is referenced by: issetf 2640 isseti 2641 issetri 2642 elex 2644 elisset 2647 vtoclg1f 2692 ceqex 2758 eueq 2800 moeq 2804 mosubt 2806 ru 2853 sbc5 2877 snprc 3527 vprc 3992 opelopabsb 4111 eusvnfb 4304 euiotaex 5030 fvmptdf 5426 fvmptdv2 5428 fmptco 5503 brabvv 5733 ovmpt2df 5814 ovi3 5819 tfrlemibxssdm 6130 tfr1onlembxssdm 6146 tfrcllembxssdm 6159 ecexr 6337 snexxph 6739 bj-vprc 12511 bj-vnex 12513 bj-2inf 12557 |
Copyright terms: Public domain | W3C validator |