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 3494)
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 7454. Note that a class 𝐴 which
is
not a set is called a proper class. In some theorems, such as
uniexg 7456, 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 2890 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 | dfclel 2891 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) | |
2 | vex 3495 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | biantru 530 | . . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
4 | 3 | exbii 1839 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V)) |
5 | 1, 4 | bitr4i 279 | 1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 Vcvv 3492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 |
This theorem is referenced by: issetf 3505 issetiOLD 3507 issetri 3508 elex 3510 elissetOLD 3513 eueq 3696 ru 3768 sbc5 3797 snprc 4645 vprc 5210 eusvnfb 5284 reusv2lem3 5291 iotaex 6328 funimaexg 6433 fvmptd3f 6775 fvmptdv2 6778 ovmpodf 7295 rankf 9211 fnpr2ob 16819 isssc 17078 snelsingles 33280 bj-snglex 34182 bj-nul 34243 dissneqlem 34503 snen1g 39768 rr-spce 40435 iotaexeu 40627 elnev 40647 ax6e2nd 40769 ax6e2ndVD 41119 ax6e2ndALT 41141 upbdrech 41448 itgsubsticclem 42136 |
Copyright terms: Public domain | W3C validator |