![]() |
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 2459 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1352 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 2148 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | cab 2163 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: rabid 2652 rabid2 2653 rabbi 2654 rabswap 2655 nfrab1 2656 nfrabxy 2657 rabbiia 2722 rabbidva2 2724 rabeqf 2727 cbvrab 2735 rabab 2758 elrabi 2890 elrabf 2891 elrab3t 2892 ralrab2 2902 rexrab2 2904 cbvrabcsf 3122 dfin5 3136 dfdif2 3137 ss2rab 3231 rabss 3232 ssrab 3233 rabss2 3238 ssrab2 3240 rabssab 3243 notab 3405 unrab 3406 inrab 3407 inrab2 3408 difrab 3409 dfrab2 3410 dfrab3 3411 notrab 3412 rabun2 3414 dfnul3 3425 rabn0r 3449 rabn0m 3450 rab0 3451 rabeq0 3452 dfif6 3536 rabsn 3658 reusn 3662 rabsneu 3664 elunirab 3820 elintrab 3854 ssintrab 3865 iunrab 3931 iinrabm 3946 intexrabim 4150 repizf2 4159 exss 4223 rabxp 4659 exse2 4997 mptpreima 5117 fndmin 5618 fncnvima2 5632 riotauni 5830 riotacl2 5837 snriota 5853 xp2 6167 unielxp 6168 dfopab2 6183 unfiexmid 6910 nnzrab 9253 nn0zrab 9254 shftlem 10796 shftuz 10797 shftdm 10802 negfi 11207 cnblcld 13668 if0ab 14179 bdcrab 14226 |
Copyright terms: Public domain | W3C validator |