![]() |
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 2379 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1298 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1448 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 103 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | cab 2086 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: rabid 2564 rabid2 2565 rabbi 2566 rabswap 2567 nfrab1 2568 nfrabxy 2569 rabbiia 2626 rabbidva2 2628 rabeqf 2631 cbvrab 2639 rabab 2662 elrabi 2790 elrabf 2791 elrab3t 2792 ralrab2 2802 rexrab2 2804 cbvrabcsf 3015 dfin5 3028 dfdif2 3029 ss2rab 3120 rabss 3121 ssrab 3122 rabss2 3127 ssrab2 3129 rabssab 3131 notab 3293 unrab 3294 inrab 3295 inrab2 3296 difrab 3297 dfrab2 3298 dfrab3 3299 notrab 3300 rabun2 3302 dfnul3 3313 rabn0r 3336 rabn0m 3337 rab0 3338 rabeq0 3339 dfif6 3423 rabsn 3537 reusn 3541 rabsneu 3543 elunirab 3696 elintrab 3730 ssintrab 3741 iunrab 3807 iinrabm 3822 intexrabim 4018 repizf2 4026 exss 4087 rabxp 4514 exse2 4849 mptpreima 4968 fndmin 5459 fncnvima2 5473 riotauni 5668 riotacl2 5675 snriota 5691 xp2 6001 unielxp 6002 dfopab2 6017 unfiexmid 6735 nnzrab 8930 nn0zrab 8931 shftlem 10429 shftuz 10430 shftdm 10435 negfi 10838 cnblcld 12457 bdcrab 12631 |
Copyright terms: Public domain | W3C validator |