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 3185 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | isset 3180 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | sylib 207 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: elex2 3189 elex22 3190 ceqsalt 3201 ceqsalgALT 3204 cgsexg 3211 cgsex2g 3212 cgsex4g 3213 vtoclgft 3227 vtoclgftOLD 3228 vtocleg 3252 vtoclegft 3253 spc2egv 3268 spc3egv 3270 tpid3gOLD 4249 iinexg 4751 ralxfr2d 4808 copsex2t 4883 copsex2g 4884 fliftf 6465 eloprabga 6645 ovmpt4g 6681 eroveu 7729 mreiincl 16079 metustfbas 22172 spc2ed 28696 eqvincg 28698 brabgaf 28800 bnj852 30245 bnj938 30261 bnj1125 30314 bnj1148 30318 bnj1154 30321 bj-csbsnlem 32090 bj-snsetex 32144 bj-snglc 32150 elex2VD 38095 elex22VD 38096 tpid3gVD 38099 |
Copyright terms: Public domain | W3C validator |