![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elisset | GIF version |
Description: An element of a class exists. (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
elisset | ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2630 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | isset 2625 | . 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | |
3 | 1, 2 | sylib 120 | 1 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1289 ∃wex 1426 ∈ wcel 1438 Vcvv 2619 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-sb 1693 df-clab 2075 df-cleq 2081 df-clel 2084 df-v 2621 |
This theorem is referenced by: elex22 2634 elex2 2635 ceqsalt 2645 ceqsalg 2647 cgsexg 2654 cgsex2g 2655 cgsex4g 2656 vtoclgft 2669 vtocleg 2690 vtoclegft 2691 spc2egv 2708 spc2gv 2709 spc3egv 2710 spc3gv 2711 eqvincg 2741 tpid3g 3555 iinexgm 3990 copsex2t 4072 copsex2g 4073 ralxfr2d 4286 rexxfr2d 4287 fliftf 5578 eloprabga 5735 ovmpt4g 5767 spc2ed 5998 eroveu 6381 supelti 6695 genpassl 7081 genpassu 7082 eqord1 7959 nn1suc 8439 bj-inex 11753 |
Copyright terms: Public domain | W3C validator |