New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 2867 | . 2 | |
2 | isset 2863 | . 2 | |
3 | 1, 2 | sylib 188 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wex 1541 wceq 1642 wcel 1710 cvv 2859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-v 2861 |
This theorem is referenced by: elex22 2870 elex2 2871 ceqsalt 2881 ceqsalg 2883 cgsexg 2890 cgsex2g 2891 cgsex4g 2892 vtoclgft 2905 vtocleg 2925 vtoclegft 2926 spc2egv 2941 spc3egv 2943 tpid3g 3831 opkelcokg 4261 copsex2t 4608 copsex2g 4609 ovmpt4g 5710 ncelncs 6120 |
Copyright terms: Public domain | W3C validator |