![]() |
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 2739)
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 4436. Note the when 𝐴 is not
a set,
it is called a proper class. In some theorems, such as uniexg 4438, 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 2173 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 2173 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 2740 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 302 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1605 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 187 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 = wceq 1353 ∃wex 1492 ∈ wcel 2148 Vcvv 2737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-v 2739 |
This theorem is referenced by: issetf 2744 isseti 2745 issetri 2746 elex 2748 elisset 2751 vtoclg1f 2796 ceqex 2864 eueq 2908 moeq 2912 mosubt 2914 ru 2961 sbc5 2986 snprc 3657 snssb 3725 vprc 4134 opelopabsb 4259 eusvnfb 4453 elrelimasn 4992 euiotaex 5192 fvmptdf 5601 fvmptdv2 5603 fmptco 5680 brabvv 5917 ovmpodf 6002 ovi3 6007 tfrlemibxssdm 6324 tfr1onlembxssdm 6340 tfrcllembxssdm 6353 ecexr 6536 snexxph 6945 bj-vprc 14499 bj-vnex 14501 bj-2inf 14541 |
Copyright terms: Public domain | W3C validator |