![]() |
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 2691)
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 4367. Note the when 𝐴 is not
a set,
it is called a proper class. In some theorems, such as uniexg 4369, 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 2136 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 2136 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 2692 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 300 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1585 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 186 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 = wceq 1332 ∃wex 1469 ∈ wcel 1481 Vcvv 2689 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-v 2691 |
This theorem is referenced by: issetf 2696 isseti 2697 issetri 2698 elex 2700 elisset 2703 vtoclg1f 2748 ceqex 2816 eueq 2859 moeq 2863 mosubt 2865 ru 2912 sbc5 2936 snprc 3596 vprc 4068 opelopabsb 4190 eusvnfb 4383 euiotaex 5112 fvmptdf 5516 fvmptdv2 5518 fmptco 5594 brabvv 5825 ovmpodf 5910 ovi3 5915 tfrlemibxssdm 6232 tfr1onlembxssdm 6248 tfrcllembxssdm 6261 ecexr 6442 snexxph 6846 bj-vprc 13265 bj-vnex 13267 bj-2inf 13307 |
Copyright terms: Public domain | W3C validator |