Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > isseti | Unicode version |
Description: A way to say " is a set" (inference form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
isseti.1 |
Ref | Expression |
---|---|
isseti |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isseti.1 | . 2 | |
2 | isset 2727 | . 2 | |
3 | 1, 2 | mpbi 144 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 wex 1479 wcel 2135 cvv 2721 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-v 2723 |
This theorem is referenced by: rexcom4b 2746 ceqsex 2759 vtoclf 2774 vtocl2 2776 vtocl3 2777 vtoclef 2794 eqvinc 2844 euind 2908 opabm 4252 eusv2nf 4428 dtruex 4530 limom 4585 isarep2 5269 dfoprab2 5880 rnoprab 5916 dmaddpq 7311 dmmulpq 7312 bj-inf2vnlem1 13687 |
Copyright terms: Public domain | W3C validator |