![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elisset | Structured version Visualization version GIF version |
Description: An element of a class exists. (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
elisset | ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3430 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | isset 3425 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | sylib 210 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∃wex 1880 ∈ wcel 2166 Vcvv 3415 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1662 df-ex 1881 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-v 3417 |
This theorem is referenced by: elex2 3434 elex22 3435 ceqsalt 3446 ceqsalgALT 3449 cgsexg 3456 cgsex2g 3457 cgsex4g 3458 vtoclgft 3472 vtocleg 3497 vtoclegft 3498 spc2egv 3513 spc3egv 3515 eqvincg 3548 iinexg 5047 ralxfr2d 5111 copsex2t 5178 copsex2g 5179 fliftf 6821 eloprabga 7008 ovmpt4g 7044 eroveu 8109 mreiincl 16610 metustfbas 22733 spc2ed 29868 brabgaf 29968 bnj852 31538 bnj938 31554 bnj1125 31607 bnj1148 31611 bnj1154 31614 bj-csbsnlem 33420 bj-snsetex 33474 bj-snglc 33480 elex2VD 39893 elex22VD 39894 tpid3gVD 39897 elsprel 42573 |
Copyright terms: Public domain | W3C validator |