![]() |
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 2472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1363 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 2160 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | cab 2175 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: rabid 2666 rabid2 2667 rabbi 2668 rabswap 2669 nfrab1 2670 nfrabxy 2671 rabbiia 2737 rabbidva2 2739 rabeqf 2742 cbvrab 2750 rabab 2773 elrabi 2905 elrabf 2906 elrab3t 2907 ralrab2 2917 rexrab2 2919 cbvrabcsf 3137 dfin5 3151 dfdif2 3152 ss2rab 3246 rabss 3247 ssrab 3248 rabss2 3253 ssrab2 3255 rabssab 3258 notab 3420 unrab 3421 inrab 3422 inrab2 3423 difrab 3424 dfrab2 3425 dfrab3 3426 notrab 3427 rabun2 3429 dfnul3 3440 rabn0r 3464 rabn0m 3465 rab0 3466 rabeq0 3467 dfif6 3551 rabsn 3674 reusn 3678 rabsneu 3680 elunirab 3837 elintrab 3871 ssintrab 3882 iunrab 3949 iinrabm 3964 intexrabim 4168 repizf2 4177 exss 4242 rabxp 4678 exse2 5017 mptpreima 5137 fndmin 5640 fncnvima2 5654 riotauni 5854 riotacl2 5861 snriota 5877 xp2 6193 unielxp 6194 dfopab2 6209 unfiexmid 6941 nnzrab 9302 nn0zrab 9303 shftlem 10852 shftuz 10853 shftdm 10858 negfi 11263 eqglact 13157 dfrhm2 13497 cnblcld 14472 if0ab 14995 bdcrab 15042 |
Copyright terms: Public domain | W3C validator |