Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > isset | Structured version Visualization version GIF version |
Description: Two ways to say
"𝐴 is a set": A class 𝐴 is a
member of the
universal class V (see df-v 3175)
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 6851. Note the when 𝐴 is not
a set,
it is called a proper class. In some theorems, such as uniexg 6853, 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 2606 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 2606 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 3176 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 525 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1764 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 266 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 |
This theorem is referenced by: issetf 3181 isseti 3182 issetri 3183 elex 3185 elisset 3188 vtoclg1f 3238 eueq 3345 moeq 3349 ru 3401 sbc5 3427 snprc 4197 vprc 4724 vnex 4726 eusvnfb 4788 reusv2lem3 4797 iotaex 5785 funimaexg 5889 fvmptdf 6204 fvmptdv2 6206 ovmpt2df 6690 rankf 8540 isssc 16303 snelsingles 31199 bj-snglex 32154 bj-nul 32209 dissneqlem 32363 iotaexeu 37641 elnev 37661 ax6e2nd 37795 ax6e2ndVD 38166 ax6e2ndALT 38188 upbdrech 38460 itgsubsticclem 38867 |
Copyright terms: Public domain | W3C validator |