![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elisset | Unicode version |
Description: An element of a class exists. (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
elisset |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2666 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | isset 2661 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 121 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-v 2657 |
This theorem is referenced by: elex22 2670 elex2 2671 ceqsalt 2681 ceqsalg 2683 cgsexg 2690 cgsex2g 2691 cgsex4g 2692 vtoclgft 2705 vtocleg 2726 vtoclegft 2727 spc2egv 2744 spc2gv 2745 spc3egv 2746 spc3gv 2747 eqvincg 2777 tpid3g 3602 iinexgm 4037 copsex2t 4125 copsex2g 4126 ralxfr2d 4343 rexxfr2d 4344 fliftf 5652 eloprabga 5810 ovmpt4g 5845 spc2ed 6082 eroveu 6472 supelti 6839 genpassl 7274 genpassu 7275 eqord1 8158 nn1suc 8643 bj-inex 12788 |
Copyright terms: Public domain | W3C validator |