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.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.) |
Ref | Expression |
---|---|
elisset | ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exsimpl 1860 | . 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦 𝑦 = 𝐴) | |
2 | dfclel 2891 | . 2 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉)) | |
3 | eqeq1 2822 | . . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴)) | |
4 | 3 | cbvexvw 2035 | . 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴) |
5 | 1, 2, 4 | 3imtr4i 293 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 |
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-cleq 2811 df-clel 2890 |
This theorem is referenced by: isseti 3506 elex2 3514 elex22 3515 ceqsalt 3525 ceqsalgALT 3528 cgsexg 3535 cgsex2g 3536 cgsex4g 3537 vtoclgft 3551 vtoclgftOLD 3552 vtoclg1f 3564 vtocleg 3578 vtoclegft 3579 spcimdv 3589 spcegv 3594 spc2egv 3597 spc2ed 3599 eqvincg 3638 iinexg 5235 ralxfr2d 5301 copsex2t 5374 copsex2g 5375 dmopab2rex 5779 fliftf 7057 eloprabga 7250 ovmpt4g 7286 eroveu 8381 mreiincl 16855 metustfbas 23094 brabgaf 30287 bnj852 32092 bnj938 32108 bnj1125 32161 bnj1148 32165 bnj1154 32168 dmopab3rexdif 32549 bj-csbsnlem 34117 bj-snsetex 34172 bj-snglc 34178 copsex2d 34323 prjspeclsp 39140 elex2VD 41049 elex22VD 41050 tpid3gVD 41053 elsprel 43514 |
Copyright terms: Public domain | W3C validator |