![]() |
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. Use elissetv 2806 instead when sufficient (for instance in usages where 𝑥 is a dummy variable). (Contributed by NM, 1-May-1995.) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019.) |
Ref | Expression |
---|---|
elisset | ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elissetv 2806 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴) | |
2 | vextru 2709 | . . . 4 ⊢ 𝑦 ∈ {𝑧 ∣ ⊤} | |
3 | 2 | issetlem 2805 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑦 𝑦 = 𝐴) |
4 | vextru 2709 | . . . 4 ⊢ 𝑥 ∈ {𝑧 ∣ ⊤} | |
5 | 4 | issetlem 2805 | . . 3 ⊢ (𝐴 ∈ {𝑧 ∣ ⊤} ↔ ∃𝑥 𝑥 = 𝐴) |
6 | 3, 5 | bitr3i 276 | . 2 ⊢ (∃𝑦 𝑦 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴) |
7 | 1, 6 | sylib 217 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ⊤wtru 1534 ∃wex 1773 ∈ wcel 2098 {cab 2702 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-clel 2802 |
This theorem is referenced by: elex2OLD 3485 ceqsalt 3495 ceqsalgALT 3498 cgsexg 3508 cgsex2g 3509 cgsex4g 3510 cgsex4gOLD 3511 cgsex4gOLDOLD 3512 vtocleg 3532 vtocld 3540 vtoclg1f 3550 vtoclgOLD 3551 vtoclegftOLD 3570 spcimdv 3578 spcegv 3582 spc2egv 3584 spc2ed 3586 eqvincg 3632 clel2g 3643 clel4g 3648 elabd2 3656 elabgt 3658 elabgtOLD 3659 elabg 3663 ralsng 4681 dfiun2g 5037 iinexg 5347 ralxfr2d 5413 copsex2t 5497 copsex2gOLD 5499 dmopab2rex 5923 fliftf 7326 eloprabga 7532 eloprabgaOLD 7533 ovmpt4g 7572 eroveu 8840 mreiincl 17604 metustfbas 24549 brabgaf 32519 bnj852 34722 bnj938 34738 bnj1125 34793 bnj1148 34797 bnj1154 34800 fineqvpow 34886 dmopab3rexdif 35185 rexxfr3dALT 35419 bj-isseti 36532 bj-ceqsalt 36540 bj-ceqsalg 36543 bj-spcimdv 36549 bj-csbsnlem 36557 bj-vtoclg1f 36572 bj-snsetex 36618 bj-snglc 36624 bj-clel3gALT 36703 copsex2d 36794 prjspeclsp 42203 elex2VD 44451 elex22VD 44452 tpid3gVD 44455 elsprel 46984 |
Copyright terms: Public domain | W3C validator |