![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-rab | Unicode version |
Description: Define a restricted class
abstraction (class builder), which is the class
of all ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-rab |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | cA |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | crab 2357 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1284 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1434 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 102 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | cab 2069 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: rabid 2534 rabid2 2535 rabbi 2536 rabswap 2537 nfrab1 2538 nfrabxy 2539 rabbiia 2596 rabeqf 2600 cbvrab 2608 rabab 2629 elrabi 2754 elrabf 2755 elrab3t 2756 ralrab2 2766 rexrab2 2768 cbvrabcsf 2976 dfin5 2989 dfdif2 2990 ss2rab 3079 rabss 3080 ssrab 3081 rabss2 3086 ssrab2 3088 rabssab 3090 notab 3250 unrab 3251 inrab 3252 inrab2 3253 difrab 3254 dfrab2 3255 dfrab3 3256 notrab 3257 rabun2 3259 dfnul3 3270 rabn0r 3287 rabn0m 3288 rab0 3289 rabeq0 3290 dfif6 3370 rabsn 3477 reusn 3481 rabsneu 3483 elunirab 3634 elintrab 3668 ssintrab 3679 iunrab 3745 iinrabm 3760 intexrabim 3948 repizf2 3956 exss 4010 rabxp 4426 exse2 4749 mptpreima 4864 fndmin 5326 fncnvima2 5340 riotauni 5525 riotacl2 5532 snriota 5548 xp2 5850 unielxp 5851 dfopab2 5866 unfiexmid 6462 nnzrab 8508 nn0zrab 8509 shftlem 9905 shftuz 9906 shftdm 9911 negfi 10311 bdcrab 10910 |
Copyright terms: Public domain | W3C validator |