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 2687 | . 2 | |
3 | 1, 2 | mpbi 144 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1331 wex 1468 wcel 1480 cvv 2681 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-v 2683 |
This theorem is referenced by: rexcom4b 2706 ceqsex 2719 vtoclf 2734 vtocl2 2736 vtocl3 2737 vtoclef 2754 eqvinc 2803 euind 2866 opabm 4197 eusv2nf 4372 dtruex 4469 limom 4522 isarep2 5205 dfoprab2 5811 rnoprab 5847 dmaddpq 7180 dmmulpq 7181 bj-inf2vnlem1 13157 |
Copyright terms: Public domain | W3C validator |