![]() |
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 3353)
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 7098. Note that a class 𝐴 which
is
not a set is called a proper class. In some theorems, such as
uniexg 7100, 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 2767 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 2767 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 3354 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 519 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1924 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 267 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 = wceq 1631 ∃wex 1852 ∈ wcel 2145 Vcvv 3351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-tru 1634 df-ex 1853 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-v 3353 |
This theorem is referenced by: issetf 3360 isseti 3361 issetri 3362 elex 3364 elisset 3367 vtoclg1f 3416 eueq 3530 moeq 3534 ru 3586 sbc5 3612 snprc 4389 vprc 4931 eusvnfb 4993 reusv2lem3 5000 iotaex 6009 funimaexg 6113 fvmptd3f 6435 fvmptdv2 6438 ovmpt2df 6937 rankf 8819 isssc 16680 dmscut 32248 snelsingles 32359 bj-snglex 33285 bj-nul 33342 dissneqlem 33517 iotaexeu 39138 elnev 39158 ax6e2nd 39292 ax6e2ndVD 39659 ax6e2ndALT 39681 upbdrech 40029 itgsubsticclem 40701 |
Copyright terms: Public domain | W3C validator |