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 2566 | . 2 | |
2 | isset 2561 | . 2 | |
3 | 1, 2 | sylib 127 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 wex 1381 wcel 1393 cvv 2557 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-v 2559 |
This theorem is referenced by: elex22 2569 elex2 2570 ceqsalt 2580 ceqsalg 2582 cgsexg 2589 cgsex2g 2590 cgsex4g 2591 vtoclgft 2604 vtocleg 2624 vtoclegft 2625 spc2egv 2642 spc2gv 2643 spc3egv 2644 spc3gv 2645 eqvincg 2668 tpid3g 3483 iinexgm 3908 copsex2t 3982 copsex2g 3983 ralxfr2d 4196 rexxfr2d 4197 fliftf 5439 eloprabga 5591 ovmpt4g 5623 eroveu 6197 genpassl 6622 genpassu 6623 nn1suc 7933 bj-inex 10027 |
Copyright terms: Public domain | W3C validator |