| 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 2822 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 2822 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴) | |
| 2 | iseqsetv-clel 2820 | . 2 ⊢ (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴) | |
| 3 | 1, 2 | sylib 218 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∃wex 1779 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-clel 2816 |
| This theorem is referenced by: elex2OLD 3505 ceqsalt 3515 ceqsalgALT 3518 cgsexg 3526 cgsex2g 3527 cgsex4g 3528 cgsex4gOLD 3529 vtocleg 3553 vtocld 3561 vtoclg1f 3570 vtoclgOLD 3571 vtoclegftOLD 3589 spcimdv 3593 spcegv 3597 spc2egv 3599 spc2ed 3601 eqvincg 3648 clel2g 3659 clel4g 3663 elabd2 3670 elabgt 3672 elabgtOLD 3673 elabg 3676 ralsng 4675 dfiun2g 5030 iinexg 5348 ralxfr2d 5410 copsex2t 5497 dmopab2rex 5928 fliftf 7335 eloprabga 7542 ovmpt4g 7580 eroveu 8852 mreiincl 17639 metustfbas 24570 brabgaf 32620 bnj852 34935 bnj938 34951 bnj1125 35006 bnj1148 35010 bnj1154 35013 fineqvpow 35110 dmopab3rexdif 35410 rexxfr3dALT 35644 bj-isseti 36879 bj-ceqsalt 36887 bj-ceqsalg 36890 bj-spcimdv 36896 bj-csbsnlem 36904 bj-vtoclg1f 36919 bj-snsetex 36964 bj-snglc 36970 bj-clel3gALT 37049 copsex2d 37140 prjspeclsp 42622 elex2VD 44858 elex22VD 44859 tpid3gVD 44862 elsprel 47462 |
| Copyright terms: Public domain | W3C validator |